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


Reading suggestions