This year, the course is given by Benjamin Werner
Sept. 18. Introduction, first-order logic, natural deduction and deduction modulo. Slides: handout and with animation.
Coq live coding examples
Sept. 25.
Cuts in Heyting Arithmetic Slides.
Class files: TD1-23.v and
solution: TD1-23_sol.v.
Oct. 2.
Higher-Order Logic and inductive properties.
Exercise sheet (pdf) and
some solutions.
Coq exercices and solutions.
Oct. 9th. Functions in Higher-Order Logic; System T Slides for print.
Oct. 16.
Curry-Howard Isomorphism.
Coq exercices: here>.
Oct. 23.
Martin-Löf's Type Theory
Oct. 30.
Universes and computational proofs is MLTT - slides.
System F
Nov. 6.
F omega, PTSs, Calculus of Constructions
Slides>.