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 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.
Arthur Charguéraud, Adam Chlipala, Andres Erbsen, Samuel Gruetter
TOPLAS: ACM Transactions on Programming Languages and Systems, March 2023
Martin Bodin, Arthur Charguéraud, Daniele Filaretti, Philippa Gardner, Sergio Maffeis, Daiva Naudziuniene, Alan Schmitt and Gareth Smith
POPL: Symposium on Principles of Programming Languages, January 2014
ESOP: European Symposium on Programming, March 2013
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