Foundations of Proof Systems

MPRI - course PRFSYS

2025-26

This year's exam and the solution.

This year, the course is given by Benjamin Werner

Exam date: November, 25th (probably 16:30 - 18:30). Course Notes, slide printouts and personal notes are authorized.

Course Notes

Here (not yet updated).
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.

Bootstraping Project

Proposal to start a collective and distributed project: bootstraping PRFSYS. A Git account. Please write me to ask for obtaining writing rights.

Schedule 2025

  • Sept. 16th. Introduction and motivations. First-order logic and deduction. Logical and Axiomatical Cuts in Arithmetic. Slides: handout.

    Rocq live coding examples


    Class files: TD1.v and solution: TD1_sol.v.

    Comment: the point is to "see" the natural deduction proof steps, and how computations are used in the proofs. The beginning are some simple examples. For students not used to Rocq, you may want to look, for instance, at "Coq in a hurry". Feel free to suggest other crash courses or references !

  • Sept. 23. Cuts in Arithmetic. Slides handout.

    Class files: td2_exo.v and solution. More exotic: exercises about the epsilon operator and solution.

  • Sept. 30. Higher-Order Logic. Slides handout.

    Class files: impred.v and solution.

  • Oct. 7. Functions in Higher-Order Logic; Normalization and reducibility.
    Slides handout. (Not many slides; look at the course notes for the normaliation proof).

  • Oct. 14th. Dependent Types print.

    • Class files: exercises about Curry-Howad CH_2025.v and solution.

  • Oct. 21st. Martin-Löf's Type Theory. Slides.
    Class file: here. solution

  • Nov. 4th. System F, PTSs, computational proofs.
    Slides here. Class file: here. solution

  • Nov. 18th. About Stronger Type Theories like Rocq's, Prop/Set distiction, limitations and some paradoxes. Slides here.
    Class file: here. solution and slight rephasing of solution. Vanilla Rocq solution

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