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

• Slides

Tutorial

• Exercise sheet
• Online Coq tutorial (requires Firefox ≥ 45 or Chrome ≥ 48)
• Raw Coq file (requires to have Coq installed on your computer)
• Solutions (for the Coq part)

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

• Slides
• Coq: Examples on inductive types
• Coq: Proof of Glivenko's theorem
• Coq: Examples on dependent types

Misc

• Download Coq (there are also Debian packages: coq and coqide)
• Course notes by Andreas Abel (in German)

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.