Foundations
of Proof Systems
MPRI
- course 2-7-1
2014
This
year, the course is given by Benjamin
Werner; it will be followed by the courses 2-7-2 which is more
centered on the Coq proof system and 2-36-1 on formal program
correctness proofs.
Schedule
:
- Sept.
17. Introduction, intuitionistic logic.
- Sept.
24. Cuts, cut elimination, cut-free proofs.
- Oct.
1st. Axiomatic Cuts, Deduction Modulo
Exercices:
sheet, solution
(with nice tricks, standart Coq), solution
(SSR Coq).
- Oct.
8. Going Higher-Order : naive Set theory, Higher-Order Logic,
impredicative encodings.
Exercices:
sheet, solutions
(standart Coq), solution
(SSR Coq; not much more going on in this example though).
- Oct.
15. Reducibility, normalization, System T.
Exercices, solution.
- Oct.
22. Curry-Howard correspondence for cut-elimination
- Oct.
29. Dependent types and Martin-Lof's Type Theory. Exercices, solutions.
- Nov.
5. System F. Exercices, solution.
- Nov.
12. Classical Curry-Howard.
Notes (pdf).
- Nov.
19. The Calculus of
Constructions. Exercices (pdf)
Previous Examination texts are available here
Links
:
Vidéos pour la
culture générale :