Foundations of Proof Systems

MPRI - course 2-7-1


This year's exam and the solutions.

This year, the course is given by Benjamin Werner

Slack forum 2021

Invitation Link


  • Sept. 14. Introduction, first-order logic, natural deduction and deduction modulo.

  • Sept. 21. Cuts in Heyting Arithmetic Slides. Simply typed lambda-calculus.

  • Sep. 28. Higher-Order Logic and inductive properties.
    Slides. Coq exercices

  • Oct. 5th. Functions in Higher-Order Logic. Slides for print or with animation steps
    Coq exercices

  • Oct. 12.
    Curry-Howard Isomorphism.
    Coq exercices: here and solutions.

  • Oct. 19.
    Martin-Löf's Type Theory

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. This year it is rather low/