In this tutorial, we will present the MetaCoq library of Coq and the meta-programming features it provides. MetaCoq allows users to write meta-programs on Coq terms and to specify and verify those programs w.r.t. the metatheory of Coq, which is formalized in MetaCoq. Beyond the metatheory of Coq, MetaCoq also includes a verified type-checker and a verified erasure procedure from Coq to untyped lambda-calculus. The objective of this tutorial is to give an overview of the library and focus on its features for the development of plugins and tactics inside Coq. We will present an example plugin development and let you exercise implementing your own meta-programs. To give you the tools to verify your meta-programs, we will also provide an overview of the metatheory formalized in MetaCoq that can be used to show correctness (e.g. type-preservation) of a meta-program.

More information: https://github.com/MetaCoq/metacoq/wiki/MetaCoq-Tutorial-@-POPL%C2%A02024:-Meta%E2%80%90programming-and-proving-with-MetaCoq