Computer-aided formal reasoning course

The main teachers of this course are Prof. Martin Hofmann and Dr. Gordon Cichon.
I take care of the two Coq related lectures (19/05 and 01/06), and the associated tutorial (20/05).
This page contains all the materials used during the course, along with some other potentially useful stuff.

19/05's lecture : Curry-Howard Correspondence


01/06's lecture : Inductive Types & Dependent Types


Reading suggestions

  • About Coq: CPDT, by Adam Chlipala.
  • About Curry-Howard: Proofs and Types by J.-Y. Girard, P. Taylor, Y. Lafont.
  • About dependent types: Chapter 10 of Gilles Dowek's course notes.
  • About inductive types: this tutorial by Eduardo Giménez and Pierre Castéran.