Aaron Stump's solution

• Author: Aaron Stump
• Parts addressed: 1a.
• Proof assistant / theorem prover used: Coq.
• Encoding technique: Named.
• Files: available from the author's page.

Commentary

The thesis of this solution to the POPLmark challenge is that programming language meta-theory can be feasibly formalized, at least in some cases, using names to represent bound variables. There are two main advantages of using names for bound variables. First, the representation of terms is more faithful to the official syntax of the language. Papers describing languages with bound variables, and tools implementing such languages, typically support an input syntax with named variables. Internally they may change representations of terms, but externally they support named variables. Hence, any formal meta-theory done with a representational technique like de Bruijn indices applies directly just to a possible internal representation of terms, not to terms as officially supported. Second, representing bound variables using names avoids the tedious technical complexities often associated with de Bruijn indices. It is perhaps believed that those complexities are to be preferred to the complexities associated with bound variables, for example those arising from the definition of capture-avoiding substitution. The present solution aims to show that at least in some cases, such complexities can be tamed, yielding an approach with similar or perhaps less technical tedium than de Bruijn indices.