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.
Quick jump
At the center of this project is the TemplateCoq quoting library for Coq. The project currently has a single repository extending TemplateCoq with additional features:
TemplateCoq
TemplateCoq is a quoting library for Coq. It
takes Coq
terms and constructs a representation of their syntax tree as
a Coq
inductive data type. The representation is based on the kernel’s
term representation.
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.
Checker
A partial typechecker for the Calculus of Inductive Constructions,
whose extraction to ML is runable as a plugin (using command MetaCoq
Check foo
). This checker uses fuel, so it must be passed a number
of maximal reduction steps to perfom when calling conversion, and is
NOT verified.
PCUIC
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.
Safe Checker
Implementation of a fuelfree 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 welltyped terms. The extracted safe checker is available in Coq through a new vernacular command:
MetaCoq SafeCheck <term>
After importing MetaCoq.SafeChecker.Loader
.
To roughly compare the time used to check a definition with Coq’s vanila typechecker, one can use:
MetaCoq CoqCheck <term>
Erasure
An erasure procedure to untyped lambdacalculus 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>
After importing MetaCoq.Erasure.Loader
.
Translations
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
Documentation
 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 testsuite/add_constructor.v
 The testsuite files testsuite/erasure_test.v and testsuite/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:

ident
is the type of identifiers, they should not contains any dot. E.g.nat

qualid
is the type of partially qualified names. E.g.Datatypes.nat

kername
is the type of fully qualified names. E.g.Coq.Init.Datatypes.nat
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.
Options
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.
Papers

“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 callbyvalue λ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 MetaProgramming with Typed TemplateCoq” 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) 20142019 Gregory Malecha
Copyright (c) 20152019 Abhishek Anand, Matthieu Sozeau
Copyright (c) 20172019 Simon Boulier, Nicolas Tabareau, Cyril Cohen
Copyright (c) 20182019 Danil Annenkov, Yannick Forster, Théo Winterhalter
This software is distributed under the terms of the MIT license. See LICENSE for details.
Bugs
Please report any bugs (or feature requests) on the github issue tracker.
Branches
The coq8.9 branch is the active development branch. If possible, it’s strongly recommended to use this branch.
The branches coq8.6, coq8.7 are frozen. coq8.8 is also available.
The branch master tracks the current Coq master
branch.
(Currently not working)
Installation instructions
Installing with OPAM
The easiest way to get all packages is through opam
.
To add the Coq repository to available opam
packages, use:
# opam repo add coqreleased https://coq.inria.fr/opam/released
Then, simply issue:
# opam install coqmetacoq
MetaCoq is split into multiple packages that get all installed using the
coqmetacoq
metapackage:
coqmetacoqtemplate
for the Template Monad and quoting plugincoqmetacoqchecker
for the UNverified checker of templatecoq termscoqmetacoqpcuic
for the PCUIC development and proof of the TemplateCoq > PCUIC translationcoqmetacoqsafechecker
for the verified checker on PCUIC termscoqmetacoqerasure
for the verifed erasure from PCUIC to untyped lambdacalculus.coqmetacoqtranslations
for example translations from type theory to type theory: e.g. variants of parametricity.
The 1.0alpha
versions of the package are for Coq 8.8
and Coq 8.9
.
There are also .dev
packages available in the extradev
repository
of Coq, to get those you will need to activate the following repositories:
opam repo add coqcoredev https://coq.inria.fr/opam/coredev
opam repo add coqextradev https://coq.inria.fr/opam/extradev
Old, deprecated standalone packages templatecoq2.1~beta
and
templatecoq2.1~beta3
including previous versions of templatecoq
and parts of the MetaCoq development are for Coq 8.8.
Package templatecoq2.0~beta
is for Coq 8.7.
Setting up an opam
switch
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
Equations
.
# 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
basic OCaml
4.07.1
compiler, and puts you in the right environment
(check with ocamlc v
).
Once in the right switch, you can install Coq
and the Equations
package using:
# opam pin add coq 8.9.1
# opam pin add coqequations 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 coq
available (check with coqc v
). Then simply use:
# opam install coqmetacoq
Installing from GitHub repository (for developers)
To get the source code:
# git clone https://github.com/MetaCoq/metacoq.git
# git checkout b coq8.9 origin/coq8.9
# git status
This checks that you are indeed on the coq8.9
branch.
You can create a local switch for developing using (in the root directory of the sources):
# opam switch create . 4.07.1
Or use opam switch link foo
to link an existing opam
switch foo
with
the sources directory.
Requirements
To compile the library, you need:
Coq 8.9.1
(for thecoq8.9
branch) orCoq 8.8.2
(for thecoq8.8
branch). Older versions of8.9
or8.8
might also work.OCaml
(tested with4.06.1
and4.07.1
, beware thatOCaml 4.06.0
can produce linking errors on some platforms)Equations 1.2
When using opam
you can get those using opam install depsonly .
.
You can test the installation of the packages locally using
# opam install .
at the root directory.
Compiling from sources
To compile locally without using opam
, use ./configure.sh local
at the root, then use:

make
to compile thetemplatecoq
plugin, thechecker
, thepcuic
development and thesafechecker
anderasure
plugins. You can also selectively build each target. 
make translations
to compile the translation plugins 
make testsuite
to compile the test suite 
make install
to install the plugin inCoq
’susercontrib
local library. Then theMetaCoq
namespace can be used forRequire Import
statements, e.g.From MetaCoq.Template Require Import All.
.