Foundations of Proof Systems

MPRI - course 2-7-1

2024

This year, the course is given by Benjamin Werner

Course Notes

Here (updated but should be completed).
The notes for Samuel Mimram's course go much further than a M1 course and are of interest: here.
The course notes of Gilles Dowek.

Schedule

  • Sept. 17. Introduction, first-order logic, natural deduction and deduction modulo. Logical and Aximatical Cuts in Arithmetic. Slides: handout.

    Coq live coding examples


    • Sept. 24. Higher-Order Logic. Slides: handout.

    Class files: impred.v and epsilon.v

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

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

  • Oct. 8th. Dependent Types print.

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 Coq changes depending of the years.
fleurs