The
MetaCoq project aims to provide a certified meta-programming environment in
Coq. It builds on
Template-Coq, a plugin for
Coq originally implemented by Malecha (Extensible proof engineering in intensional type theory, Harvard University,
http://gmalecha.github.io/publication/2015/02/01/extensible-proof-engineering-in-intensional-type-theory.html, 2014), which provided a reifier for
Coq terms and global declarations, as represented in the
Coq kernel, as well as a denotation command. Recently, it was used in the
CertiCoq certified compiler project (Anand et al., in: CoqPL, Paris, France,
http://conf.researchr.org/event/CoqPL-2017/main-certicoq-a-verified-compiler-for-coq, 2017), as its front-end language, to derive parametricity properties (Anand and Morrisett, in: CoqPL’18, Los Angeles, CA, USA, 2018). However, the syntax lacked semantics, be it typing semantics or operational semantics, which should reflect, as formal specifications in
Coq, the semantics of
Coq ’s type theory itself. The tool was also rather bare bones, providing only rudimentary quoting and unquoting commands. We generalize it to handle the entire polymorphic calculus of cumulative inductive constructions, as implemented by
Coq, including the kernel’s declaration structures for definitions and inductives, and implement a monad for general manipulation of
Coq ’s logical environment. We demonstrate how this setup allows
Coq users to define many kinds of general purpose plugins, whose correctness can be readily proved in the system itself, and that can be run efficiently after extraction. We give a few examples of implemented plugins, including a parametricity translation and a certified extraction to call-by-value
\(\lambda \)-calculus. We also advocate the use of
MetaCoq as a foundation for higher-level tools.