-
Notifications
You must be signed in to change notification settings - Fork 81
MetaCoq Tutorial @ POPL 2024: Meta‐programming and proving with MetaCoq
Date: Sunday, January 14th
Time: 09:00 - 12:30
In this tutorial, we will present the MetaCoq library of Coq and the features for certified meta-programming 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. MetaCoq includes in particular a verified type-checker for a large fragment of Coq and a verified erasure procedure from Coq to untyped lambda-calculus. The objective of this tutorial is to give an overview of the library. It focuses on MetaCoq's features for the development of plugins and tactics inside Coq. The tutorial will consist of four parts:
-
An introduction to the goals of the project
-
A tour of the formalized metatheory of Coq: the typing judgement and its main properties, the challenges of writing a sound and complete type-checker for it, and the verified extraction procedure to OCaml.
-
An introduction to the Template Monad for the development of meta-programs manipulating the AST of Coq terms and for interacting with the environment and the Coq kernel. We will present a simple example of a transformation in an interactive plugin development session.
-
A hands-on exercise session, aimed at writing simple meta-programs.
Attendance either physically with a POPL registration, or remotely via Zoom. Please send an email before Friday, January 12th to get access to the Zoom room.
We require all users to install the coq-metacoq-template package via opam. (Exact version TBA)
If you do not have Coq installed yet, we recommend using the Coq platform to install.
If you do not already have an editor for Coq installed, we recommend using VSCode with the VSCoq legacy plugin.
If you have trouble installing, please ask questions on MetaCoq's zulip channel.
- 09:00 - 09:10 Installation and debugging
- 09:10 - 09:30 Introduction to the project
- 09:30 - 10:15 The MetaCoq formalizations
- 10:15 - 10:30 The TemplateCoq monad
- 10:30 - 11:00 Break
- 11:00 - 11:30 Live programming in MetaCoq
- 11:30 - 12:30 Exercise session
If you know in advance that you are attending the tutorial, we kindly ask you to edit this page and fill in your name and attendance mode here:
- Tomas Diaz, in person
- Mara Malewski, in person