# 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

## 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.