CEA-EDF-INRIA summer school, INRIA Paris-Rocquencourt, Antenne Parisienne, 14-18 November 2011.
Speakers: Yves Bertot, Pierre Casteran, Benjamin Gregoire, Pierre Letouzey, Assia Mahboubi.
Venue: INRIA Antenne de Paris, 23 avenue d'Italie, 75013 Paris. Metro: Place d'Italie (lines 5,6,7). Access plan.
Room planning: Monday, salle bleue (5th floor); Tuesday, salle Algorithme (IRILL, 3rd floor); Wednesday, salle orange (5th floor); Thursday, salle verte (5th floor), Friday, salle Algorithme (IRILL, 3rd floor).
How to install Coq on your machine The Coq Proof Assistant can be downloaded from here. The files of these lectures have been tested with version 8.3 but should work with any later version. Documentation can be found here.Be sure to install also the CoqIde graphical interface (recommended). If you are familiar with Emacs, you may want to run Coq inside Proof General.
Disclaimer: working with Coq (more in general, working with proof assistants) can be extremely frustrating. If you are stuck on one exercise, do not hesitate to ask for help.
Slides and exercices Short introduction (Zappa Nardelli): slides.
Lecture 1 (Gregoire) -- Programming with natural numbers and lists in Coq -- slides, exercices, solutions.
Lecture 2 (Letouzey) -- Proposition and predicates -- slides, exercices, solutions.
Lecture 3 (Bertot) -- Making proofs in Coq -- slides, exercices.
Lecture 4 (Mahboubi) -- Proofs about programs -- slides, sources, exercices, solutions.
Lecture 5 (Mahboubi) -- Inductive data types -- slides, exercices, solutions.
Lecture 6 (Bertot) -- Inductive properties -- slides, exercices, solutions.
Lecture 7 (Letouzey) -- Dependent types -- slides, exercices.
Lecture 8 (Casteran) -- Inductive properties (ctd) -- slides, sources, exercices, solutions.
Lecture 9 (Gregoire) -- General recursion -- slides, sources, exercices, solutions.
Lecture 10 (Casteran) -- Type classes and relations -- slides, sources, exercices, solutions.
Bonus exercise: certify a compiler for a simple arithmetic language (and its solution).
All the files above in a .tar.gz archive.