of Proof Systems
- course 2-7-1
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
17. Introduction, intuitionistic logic.
24. Cuts, cut elimination, cut-free proofs.
1st. Axiomatic Cuts, Deduction Modulo
(with nice tricks, standart Coq), solution
8. Going Higher-Order : naive Set theory, Higher-Order Logic,
(standart Coq), solution
(SSR Coq; not much more going on in this example though).
15. Reducibility, normalization, System T.
22. Curry-Howard correspondence for cut-elimination
29. Dependent types and Martin-Lof's Type Theory. Exercices, solutions.
5. System F. Exercices, solution.
12. Classical Curry-Howard.
19. The Calculus of
Constructions. Exercices (pdf)
Previous Examination texts are available here |
: Dec 3rd, 16:15
Vidéos pour la
culture générale :