MetaCoq Tutorial - Meta-programming and Proving with MetaCoq

Dive into the world of meta-programming and metatheory verification with this comprehensive tutorial on the MetaCoq library for Coq. Learn how to write meta-programs on Coq terms and specify and verify them against Coq's formalized metatheory. Explore the library's features for developing plugins and tactics within Coq, including hands-on exercises to implement your own meta-programs. Gain insights into MetaCoq's verified type-checker and erasure procedure from Coq to untyped lambda-calculus. Discover how to leverage the formalized metatheory in MetaCoq to demonstrate the correctness and type-preservation of your meta-programs. This 3.5-hour tutorial, presented by experts Yannick Forster, Meven Lennon-Bertrand, Matthieu Sozeau, and Theo Winterhalter, offers a deep dive into advanced Coq programming techniques and metatheoretical reasoning.

[TutorialFest@POPL'24] MetaCoq Tutorial