This year, the course is given by Benjamin Werner

The notes for Samuel Mimram's course go much further than a M1 course and are of interest: here.

The course notes of Gilles Dowek.

Please bring your paper!

**Sept. 18.**Introduction, first-order logic, natural deduction and deduction modulo. Slides: handout and with animation.Coq live coding examples

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

Coq exercices: here with solution
**Oct. 30.**

Universes and computational proofs is MLTT - slides.

System F

**Nov. 6.**F omega, PTSs, Calculus of Constructions Slides.