Arthur Charguéraud's locally nameless solution

• Author: Arthur Charguéraud.
• Parts addressed: 1a + lemma A.10 and type safety for STLC.
• Proof assistant / theorem prover used: Coq.
• Encoding technique: Locally nameless.
• Files: available from the author's page.

Commentary

This locally nameless formalization is the result towards which I have converged at the end of an internship focused on the POPLMark Challenge. The work took place from March to July 2006 at the University of Pennsylvania, with Benjamin Pierce and Stephanie Weirich as advisors.

This solution benefits from two nice properties:

• The proofs of the main results are short and simple to follow through: the arguments are mostly the same as in a paper proof.
• The machinery involved is rather intuitive (in the sense that it does not require the ingenuity needed with pure de-Bruijn indices), and in the same time it is not too heavy (this is probably not true of a representation fully relying on names).

Main aspects of the solution:

• It is based on a locally nameless representation. As usual with this representation, there are two substitutions involved: one for indices and another one for names.
• Environments are built as lists of bindings, but then used as sets of bindings. This makes the proofs simpler because we can "forget" about the ordering of the environment. We use this not only to capture weakening, but also to capture substitution in environment. A nice side-effect is that the narrowing lemma becomes an instance of the "preservation of subtyping through type substitution" lemma.
• In SA-all rule, the name introduced is not quantified as "exists X # E", nor as "forall X # E", but as "forall X not_in L", where L is an arbitrary list of names (note that L is introduced by the constructor SA-all, and is not a parameter of the relation). The interest of this quantification is that there is no need for a formal proof of equivariance: this SA-all rule works everywhere. (Remark: equivariance is still needed to show the adequacy of the universal quantification with respect to the existential one).
• All the subtyping rules have premises enforcing the well-formation of the arguments. Tanks to a special notation for this, it does not look too bad. The advantage is that symmetry are preserved, and it seems to simplify the proofs.
• Proofs by inductions on the size of types are replaced by proofs on the derivation of the well-formation relation, which are closer to the notion of "induction on the structure of a type".