Foundations of Proof Systems

MPRI - course 2-7-1


This year, the course is given by Benjamin Werner and Pierre-Yves Strub.

Course Notes

Here (Covers lectures 1-3; I will add some minor material in the normalization chapter).


  • Sept. 10. Introduction, inductive definitions, first-order logic.

  • Sept. 17. Arithmetic, logical and axiomatic cuts, deduction modulo.

  • Sep. 24. Higher-Order Logic, Normalization and reducibility.

Past Exams