Locally nameless representation with cofinite quantification

The 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

  • The proof scripts are available from a SVN repository. To get them, run:
    svn co svn://scm.gforge.inria.fr/svn/tlc/metatheory/branches/v2 ln
  • The developments compile with Coq v8.4.
  • The developments rely on my Coq library TLC, which provides in particular enhanced tactics, and representation for variables and finite sets of variables. The TLC library is automatically imported using the svn:externals feature.
  • The developments are distributed under the permissive MIT license.

Related publications

Engineering 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

Tutorial

Formalization of STLC: a tutorial
Coq appendix to the JAR paper
Details on tactics and automation techniques used above can be found here.

Main developments

System-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 examples

Users

I maintain a non-exhaustive list of users.