## Locally nameless representation with cofinite quantificationThe locally nameless representation with cofinite quantification is a pratical technique for representing binders in a formal settings. The locally nameless representation avoids the need for alpha-conversion and the need for shifting de Bruijn indices. The cofinite quantification is used to obtain strong induction principles. This approach has been successfully applied to formalize many type systems and semantics. ## Download- The source files are available from this GitHub repository.
git clone git@github.com:charguer/formalmetacoq.git - The developments rely on my Coq library TLC, which provides in particular enhanced tactics, and representation for variables and finite sets of variables.
- The developments are distributed under the permissive MIT license.
## Related publicationsArthur Charguéraud JAR: Journal of Automated Reasoning, May 2011 Brian Aydemir, Arthur Charguéraud, Benjamin C. Pierce, Randy Pollack, and Stephanie Weirich POPL: Symposium on Principles of Programming Languages, January 2008 ## Formal representation of variable bindingProving theorems about programming language semantics or types systems usually involves long and tedious proofs, with many uninteresting cases. However, the slightest mistake in a proof can easily compromise the soundness of the entire system. Machine-checked proofs appear as an ideal solution: they eliminate the possibility for errors in proofs, and easy proof cases can be automatically handled by brute-force proof search. Yet, the formalization of programming languages requires a formal representation of variable bindings. In paper proofs, alpha-conversion is easily dealt with by adopting Barendregt's convention (1992). Reproducing a similar style of reasoning in formal proofs has been a long-standing challenge. In 2005, based on the observation that no existing technique was practical and general enough for formally reasoning about binders, a number of researchers proposed the ## Locally nameless with cofinite quantificationThe first ingredient is the locally nameless representation, in which bound variables are represented using de Bruijn indices, whereas free variables are represented using names. This representation, whose possibility has been mentioned by de Bruijn himself (1972), is a variant of the locally named approach of McKinna and Pollack (1993). Gordon (1994) first employed the locally nameless representation, and Leroy (2005) experimented it on the POPLMark challenge . The second ingredient is the cofinite quantification, which plays a key role in making it possible to directly obtain strong induction principles. Without it, a large number of renaming lemmas are required, as experienced by Leroy in his POPLMark solution. The cofinite quantification plays a similar role as in Gabbay and Pitts' nominal logic (1999), with the difference that it is here used in a standard logic and that is is introduced directly in inductive definitions. The particular way in which we combine these two ingredients leads to concise developments that remain quite faithful to the presentation of conventional paper proofs. We have illustrated the applicability of this technique on four major developments: the formalization of ML with datatypes, references and exceptions, the formalization of System F with subtyping, the formalization of the Calculus of Constructions, and the formalization of the CPS translation. The locally nameless approach has already been adopted by dozens of researchers. A non-exhaustive list can be found at the bottom of this page. |