This page contains information about the “Proof assistants” (PRFA) course in the second year (M2) of the Parisian Master in Research in Computer Science (MPRI) taught by Yannick Forster and Théo Winterhalter.
Information will come soon.
Proof assistants have a wide range of applications from mathematical theorems (including some, like the four colour theorem, that have no proof without the use of a computer) to program verification (which can be crucial for critical software, e.g. in aviation settings or cryptography).
The PRFA course aims at bringing students to a point where they are familiar enough with one proof assistant, namely Rocq, with the objectives to have the students
To this end, the course focuses on introducing general concepts found in proof assistants through practice in the Rocq proof assistant, and also mentions aspects of the underlying type theory. A complementary introduction to type systems is part of the course Foundations of proof systems.
The course will be taught in English by default. You can still ask us questions or write the exam in French.
Do not hesitate to contact us about advice around internships in the field, starting from the beginning of the course. We know a lot of people in the field so we can help you.
The most important resources for you are:
Books to learn Rocq:
Other related documents:
This course has been taught in different formats since 1997, by Christine Paulin-Mohring, Benjamin Werner, Bruno Barras, Hugo Herbelin, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, Assia Mahboubi, Matthieu Sozeau, Yannick Forster, and Théo Winterhalter. Parts of the material we teach is taken or inspired from previous iterations of the course.