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.
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:
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 runable as a plugin (using command
Check foo). This checker uses fuel, so it must be passed a number
of maximal reduction steps to perfom 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 (partial) proofs of standard metatheoretical results:
Weakening for global declarations, weakening and substitution for local contexts.
Confluence of reduction using a notion of parallel reduction
Validity, Subject Reduction and Principality.
Implementation of a fuel-free and verified reduction machine, conversion checker and type checker for PCUIC. This relies on a postulate of strong normalisation 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 vanila 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
- You may want to start with a demo
- The 8.9 branch documentation (as light coqdoc files).
- An example Coq plugin built on the Template Monad, which can be used to add a constructor to any inductive type is in test-suite/add_constructor.v
- The test-suite files test-suite/erasure_test.v and test-suite/safechecker_test.v show example uses (and current limitations of) the verified checker and erasure.
ident vs. qualid. vs kername
MetaCoq uses three types convertible to
string which have a different intended meaning:
identis the type of identifiers, they should not contains any dot. E.g.
qualidis the type of partially qualified names. E.g.
kernameis the type of fully qualified names. E.g.
Quoting always produce fully qualified names. On the converse, unquoting allow to have only partially qualified names and rely on Coq to resolve them. The commands of the TemplateMonad also allow partially qualified names.
Set / Unset Strict Unquote Universe Mode. When this mode is on,
the unquoting of a universe level fails if this level does not exists.
Otherwise the level is added to the current context. It is on by default.
There is also an “opaque” universe
fresh_universe which is unquoted to
a fresh level when
Strict Unquote Universe Mode is off.
“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.
“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. Submitted, July 2019.
A certifying extraction with time bounds from Coq to call-by-value λ-calculus. Yannick Forster and Fabian Kunze. ITP 2019. Example
“The MetaCoq Project” Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau and Théo Winterhalter. Extended version of the ITP 2018 paper. Submitted, March 2019.
This includes a full documentation of the Template Monad.
“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
Copyright (c) 2014-2019 Gregory Malecha Copyright (c) 2015-2019 Abhishek Anand, Matthieu Sozeau Copyright (c) 2017-2019 Simon Boulier, Nicolas Tabareau, Cyril Cohen Copyright (c) 2018-2019 Danil Annenkov, Yannick Forster, Théo Winterhalter
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.
The coq-8.9 branch is the active development branch. If possible, it’s strongly recommended to use this branch.
The branches coq-8.6, coq-8.7 are frozen. coq-8.8 is also available.
The branch master tracks the current Coq
(Currently not working)
Installing with OPAM
The easiest way to get all packages is through
To add the Coq repository to available
opam packages, use:
# opam repo add coq-released https://coq.inria.fr/opam/released
Then, simply issue:
# opam install coq-metacoq
MetaCoq is split into multiple packages that get all installed using the
coq-metacoq-templatefor the Template Monad and quoting plugin
coq-metacoq-checkerfor the UNverified checker of template-coq terms
coq-metacoq-pcuicfor the PCUIC development and proof of the Template-Coq -> PCUIC translation
coq-metacoq-safecheckerfor the verified checker on PCUIC terms
coq-metacoq-erasurefor the verifed erasure from PCUIC to untyped lambda-calculus.
coq-metacoq-translationsfor example translations from type theory to type theory: e.g. variants of parametricity.
1.0alpha versions of the package are for
Coq 8.8 and
There are also
.dev packages available in the
of Coq, to get those you will need to activate the following repositories:
opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
Old, deprecated standalone packages
template-coq-2.1~beta3 including previous versions of template-coq
and parts of the MetaCoq development are for Coq 8.8.
template-coq-2.0~beta is for Coq 8.7.
Setting up an
To setup a fresh
opam installation, you might want to create a
“switch” (an environment of
opam packages) for
Coq if you don’t have
one yet. You need to use opam 2 to obtain the right version of
# opam switch create coq.8.9.1 4.07.1 # eval $(opam env)
This creates the
coq.8.9.1 switch which initially contains only the
4.07.1 compiler, and puts you in the right environment
Once in the right switch, you can install
Coq and the
Equations package using:
# opam pin add coq 8.9.1 # opam pin add coq-equations 1.2+8.9
Pinning the packages prevents
opam from trying to upgrade it afterwards, in
this switch. If the commands are successful you should have
available (check with
coqc -v). Then simply use:
# opam install coq-metacoq
Installing from GitHub repository (for developers)
To get the source code:
# git clone https://github.com/MetaCoq/metacoq.git # git checkout -b coq-8.9 origin/coq-8.9 # git status
This checks that you are indeed on the
You can create a local switch for developing using (in the root directory of the sources):
# opam switch create . 4.07.1
opam switch link foo to link an existing
the sources directory.
To compile the library, you need:
Coq 8.9.1(for the
Coq 8.8.2(for the
coq-8.8branch). Older versions of
8.8might also work.
4.07.1, beware that
OCaml 4.06.0can produce linking errors on some platforms)
opam you can get those using
opam install --deps-only ..
You can test the installation of the packages locally using
# opam install .
at the root directory.
Compiling from sources
To compile locally without using
./configure.sh local at the root, then use:
maketo compile the
pcuicdevelopment and the
erasureplugins. You can also selectively build each target.
make translationsto compile the translation plugins
make test-suiteto compile the test suite
make installto install the plugin in
user-contriblocal library. Then the
MetaCoqnamespace can be used for
Require Importstatements, e.g.
From MetaCoq.Template Require Import All..