Formalizations

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.

Related publications

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
Arthur Charguéraud
ESOP: European Symposium on Programming, March 2013
Arthur Charguéraud
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