MetaCoq is a project formalizing Coq in Coq and providing tools for manipulating Coq terms and developing certified plugins (i.e. translations, compilers or tactics) in Coq.
- Getting started
- Installation instructions
- Overview of the project
- Team & Credits
You may want to start with a demo.
The current branch documentation (as light coqdoc files).
The overview of the different parts of the project.
Overview of the project
At the center of this project is the Template-Coq quoting library for Coq. The project currently has a single repository extending Template-Coq with additional features. Each extension is in dedicated folder.
Template-Coq is a quoting library for Coq. It
Coq terms and constructs a representation of their syntax tree as
Coq inductive data type. The representation is based on the kernel’s
In addition to this representation of terms, Template Coq includes:
Reification of the environment structures, for constant and inductive declarations.
Denotation of terms and global declarations
A monad for manipulating global declarations, calling the type checker, and inserting them in the global environment, in the style of MTac.
A partial type-checker for the Calculus of Inductive Constructions,
whose extraction to ML is runnable as a plugin (using command
Check foo). This checker uses fuel, so it must be passed a number
of maximal reduction steps to perform when calling conversion, and is
PCUIC, the Polymorphic Cumulative Calculus of Inductive Constructions is a cleaned up version of the term language of Coq and its associated type system, equivalent to the one of Coq. This version of the calculus has proofs of standard metatheoretical results:
Weakening for global declarations, weakening and substitution for local contexts.
Confluence of reduction using a notion of parallel reduction
Context conversion and validity of typing.
Subject Reduction (case/cofix reduction excluded)
Principality: every typeable term has a smallest type.
Elimination restrictions: the elimination restrictions ensure that singleton elimination (from Prop to Type) is only allowed on singleton inductives in Prop.
Implementation of a fuel-free and verified reduction machine, conversion checker and type checker for PCUIC. This relies on a postulate of strong normalization of the reduction relation of PCUIC on well-typed terms. The extracted safe checker is available in Coq through a new vernacular command:
MetaCoq SafeCheck <term>
To roughly compare the time used to check a definition with Coq’s vanilla type-checker, one can use:
MetaCoq CoqCheck <term>
An erasure procedure to untyped lambda-calculus accomplishing the same as the Extraction plugin of Coq. The extracted safe erasure is available in Coq through a new vernacular command:
MetaCoq Erase <term>
Examples of translations built on top of this:
a parametricity plugin in translations/param_original.v
a plugin to negate funext in translations/times_bool_fun.v
An example Coq plugin built on the Template Monad, which can be used to add a constructor to any inductive type is in examples/add_constructor.v
“Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq” Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau and Théo Winterhalter. POPL 2020, New Orleans.
“Coq Coq Codet! Towards a Verified Toolchain for Coq in MetaCoq” Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau and Théo Winterhalter. Abstract and presentation given at the Coq Workshop 2019, September 2019.
“The MetaCoq Project” Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau and Théo Winterhalter. JAR, February 2020. Extended version of the ITP 2018 paper.
This includes a full documentation of the Template Monad and the typing rules of PCUIC.
A certifying extraction with time bounds from Coq to call-by-value λ-calculus. Yannick Forster and Fabian Kunze. ITP 2019. Example
“Towards Certified Meta-Programming with Typed Template-Coq” Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau and Nicolas Tabareau. ITP 2018.
The system was presented at Coq’PL 2018
Team & Credits
MetaCoq is developed by (left to right) Abhishek Anand, Danil Annenkov, Simon Boulier, Cyril Cohen, Yannick Forster, Meven Lennon-Bertrand, Gregory Malecha, Jakob Botsch Nielsen, Matthieu Sozeau, Nicolas Tabareau and Théo Winterhalter.
Copyright (c) 2014-2021 Gregory Malecha Copyright (c) 2015-2021 Abhishek Anand, Matthieu Sozeau Copyright (c) 2017-2021 Simon Boulier, Nicolas Tabareau, Cyril Cohen Copyright (c) 2018-2021 Danil Annenkov, Yannick Forster, Théo Winterhalter Copyright (c) 2020-2021 Jakob Botsch Nielsen, Meven Lennon-Bertrand
This software is distributed under the terms of the MIT license. See LICENSE for details.
Please report any bugs or feature requests on the github issue tracker.