Computer-Aided Formal Reasoning — Coq
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
- 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.