Dear all,
as part of POPL's TutorialFest, we will run a tutorial on MetaCoq.
The tutorial will happen on Sunday, January 14th, i.e. on the day before CPP.
> 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.
Presenters:
[Yannick Forster](https://yforster.de), Inria
[Meven Lennon-Bertrand](https://www.meven.ac/), University of Cambridge
[Matthieu Sozeau](Matthieu Sozeau :: News), Inria
[Théo Winterhalter](https://theowinterhalter.github.io/), Inria
The early registration deadline for POPL (and thus the tutorials) is Thursday, December 14th.
We invite everybody to sign up!