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.
5. Curry-Howard for
12. System F,
19. The Calculus of
Vidéos pour la
culture générale :