FormalMetaCoq: Archive of Formal Metatheory in Coq

Mechanized Semantics and Type Systems

The FormalMetaCoq library contains Coq developments formalizing programming languages, from syntax and operational semantics to type systems and interpreters. In particular, it provides a collection of representative examples illustrating the following three formalization techniques.

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. This approach has been successfully applied to formalize many type systems and semantics.
The pretty-big-step semantics is a technique for formalizing large-scale programming languages. This technique avoids a quadratic blow-up that typically arises when formalizing the semantics of exceptions and/or divergence. It has been successfully put to practice to formalize the semantics of JavaScript (ECMA5).
The omni-big-step and omni-small-step semantics are particularly handy for reasoning about nondeterministic semantics. They lead to simpler compiler correctness proofs, simpler type soundness proofs, and simpler foundational construction of a Separation Logic. Omni-big-step semantics is used in particular in my course Separation Logic Foundations.

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.
For installation instructions, check the README file.
The developments are distributed under the permissive MIT license.