Installing the Coq proof assistant
- Download and install the last version of Coq (from sources or with binaries): http://coq.inria.fr/download
- Install an IDE for interacting with Coq
- a standalone IDE distributed with Coq (easier for beginners but difficult to install on some platforms): CoqIDE
- a Emacs mode: Proof General
Lecture 1: Motivations and Examples
- Slides: lecture1.pdf
Lecture 2: Coq Crash Course
- Slides: lecture2.pdf
- Coq file with holes: lecture2_with_holes.v (to be opened with a Coq IDE)
- Coq file without holes: lecture2.v
Lecture 3
- Slides: lecture3.pdf
- Abstract interpreter (need Coq 8.3): certified_while.tar.gz
Lecture 4
- Slides: lecture4.pdf