Foundations
of Proof Systems
MPRI
 course 271
2014
This
year, the course is given by Benjamin
Werner; it will be followed by the courses 272 which is more
centered on the Coq proof system and 2361 on formal program
correctness proofs.
Schedule
:
 Sept.
17. Introduction, intuitionistic logic.
 Sept.
24. Cuts, cut elimination, cutfree proofs.
 Oct.
1st. Axiomatic Cuts, Deduction Modulo
Exercices:
sheet, solution
(with nice tricks, standart Coq), solution
(SSR Coq).
 Oct.
8. Going HigherOrder : naive Set theory, HigherOrder 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: sheet, solution.
 Oct.
22. CurryHoward correspondence for cutelimination
 Oct.
29. Dependent types and MartinLof's Type Theory.
The rules.
Exercices: Sheet, solutions.
 Nov.
5. System F.
Exercices: sheet, solution.
 Nov.
12. Classical CurryHoward.
Notes (pdf).
 Nov.
19. The Calculus of Constructions.
Exercices: Sheet (pdf), solution (vanilla Coq), solution (ssr).
 Nov. 26. Informal session about formal computational proofs.
slides (pdf).
Examination text and correction (with stupid cutandpaste typo in answer to 3.b fixed).
Previous Examination texts are available here
Links
:
 An internship subject by Hugo Herbelin.
 An internship subject by Victor Magron and Benjamin Werner
 Course Notes (hopefully
soon)
 Notes
de cours de Gilles
Dowek (français)

Course Notes by Gilles Dowek (english)
 Coq

SSreflect (or SSR for small step
reflection) an extension to Coq providing some nice proof language features and libraries.
Vidéos pour la
culture générale :