All information for the course 2024/25 iteration of the course can be found at https://mpri-prfa.github.io. Please register for the course here.

The course is taught by Yannick Forster and Théo Winterhalter.

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 course aims at bringing students to a point where they are familiar enough with one proof assistant, namely Coq, with the objectives to have the students

• to be able to use Coq in other courses,
• use Coq in an internship,
• learn other proof assistants or become an expert user of Coq via self study,
• ultimately use or study proof assistants as part of a PhD.

To this end, the course focuses on introducing general concepts found in proof assistants through practice in the Coq 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 class takes place in room 1004 from 08:45 to 11:45. The first lecture is on September 23rd.

Students must bring their own laptop with Coq installed prior to the first lecture (⚠️): we require version 8.18 together with Equations and MetaCoq installed. To that end, we assume students have installed the corresponding Coq Platform. Please don't hesitate to send us an email if you have trouble installing anything before the first lecture.

See here for precise information on how to install Coq or for which editor to use.

A background in functional programming and logic is preferable, but not mandatory or necessary to pass the lecture. Experience in using Coq is not necessary. The class is designed to be interesting both for absolute newcomers and students with background using Coq.