Foundations of Proof Systems

MPRI - course PRFSYS

2026-27

This year, the course is given by Benjamin Werner and Dominik Kirst.

Course Notes

Here (first version of 2026 (sept. 19)).
The notes for Samuel Mimram's M1 course go much further than a M1 course and are of interest: here.
The course notes of Gilles Dowek.

Schedule 2026

  • Sept. 18th. Introduction and motivations. Strong Normalization for simple type. First-order logic and deduction. Logical and Axiomatical Cuts in Arithmetic. Slides: handout.

    Rocq live coding examples


On the Side

Feel free to try this little prototype of a gestural user interface for a prover (we are happy about feedback). Here is a fun riddle.

Past Exams

Note that the content of the course fluctuates with time. Also the amount of Rocq changes depending of the years.
fleurs