LN: Locally nameless representation with cofinite quantification

Locally nameless representation with cofinite quantification

The locally nameless representation can be used to represent binders in a formal settings. In this representation, bound variables are represented using de Bruijn indices, whereas free variables are represented using names. The cofinite quantification plays a key role in making it possible to obtain strong induction principles.

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 metatheory

The developments compile both with Coq v8.3pl1 and v8.3pl2.
The metatheory library relies on the non-constructive TLC library, which not only provides powerful tactics but also allows simplification in the treatment of comparison between variables and in the representation of finite sets. This TLC library is integrated in the locally nameless library, so you do not need to install it separately.
The library and 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

paper - bib

The Locally Nameless Representation

Journal of Automated Reasoning (JAR), May 2011

paper - bib

Tutorial

Formalization of STLC: a tutorial	STLC_Core_Tutorial
Coq appendix to the JAR paper	Lambda_JAR_paper

Details on tactics and automation can be found here.

Main developments

ML with datatypes, recursion, references and exceptions Type soundness	ML_Definitions ML_Infrastructure ML_Soundness
System-Fsub: PoplMark 1A+2A Type soundness	Fsub_Definitions Fsub_Infrastructure Fsub_Soundness
Pure lambda calculus Church-Rosser property	Lambda_Definitions Lambda_Infrastructure Lambda_ChurchRosser
Call-by-value lambda calculus Correctness of the CPS translation	CPS_Definitions CPS_Infrastructure CPS_Correctness
Call-by-value lambda calculus Equivalence of big-step and small-step semantics	BigStep_Definitions BigStep_Infrastructure BigStep_Correctness
Calculus of Constructions Subject reduction	CoC_Definitions CoC_Infrastructure CoC_BetaStar CoC_ChurchRosser CoC_Conversion CoC_Preservation

Metatheory library

Metatheory Library

Additional tutorial examples

STLC Type soundness	STLC_Core_Definitions STLC_Core_Infrastructure STLC_Core_Soundness
STLC Extra material	STLC_Core_Adequacy STLC_Core_FullBeta STLC_Core_Light
STLC + Exceptions Type soundness	STLC_Exn_Definitions STLC_Exn_Infrastructure STLC_Exn_Soundness
STLC + References Type soundness	STLC_Ref_Definitions STLC_Ref_Infrastructure STLC_Ref_Soundness

Older releases

Version from July 2007 (patched for more recent version of Coq). Same development, but compiles with Coq v8.3pl1 and v8.3pl2. Available from the following svn repository.
```
svn co svn://scm.gforge.inria.fr/svn/tlc/metatheory/branches/v1 metatheory_v1
```
Version from July 2007 (original release). Compile only with Coq v8.1pl2 and v8.1pl3. Available from here.

Users

A non-exhaustive list of users of the approach locally nameless with cofinite quantification can be found here.