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.

  • Oct. 15th. System T.
    Class file: here. solution

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

  • Oct. 29th. Universes (some). System F.
    Slides (universes) here. Coq live coding here. Class file: here. solution

  • Nov. 5th. F-omega, PTSs, computational proofs. slides.
Upcoming:
Nov. 26th: Exam. At 16:30
Dec. 10th: Dead-line for the Project (please send me a little mail to notify me that you handed in something with some short description 🙏)

Internships

A first and second intership topics about Actema.

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