## 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. On this page, you willl find a collection of examples formalized in Coq using this approach. ## Download## Related publicationsEngineering Formal Metatheory with B. Aydemir, B. C. Pierce, R. Pollack and S. Weirich Symposium on Principles of Programming Languages (POPL), January 2008 The Locally Nameless Representation Journal of Automated Reasoning (JAR), May 2011 ## TutorialFormalization of STLC: a tutorial | | Coq appendix to the JAR paper | |
Details on tactics and automation techniques used above can be found here. ## Main developmentsSystem-Fsub (PoplMark 1A+2A) Type soundness | | ML with data types, recursion, references and exceptions Type soundness | | Pure lambda calculus Church-Rosser property | | Call-by-value lambda calculus Correctness of the CPS translation | | Call-by-value lambda calculus Equivalence of big-step and small-step semantics | | Calculus of Constructions Subject reduction | |
## Additional tutorial examplesSTLC Type soundness | | STLC Extra material | | STLC + Exceptions Type soundness | | STLC + References Type soundness | |
## Users |