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 .
Class files: TD1-23.v and
solution: TD1-23_sol.v.