Modelling and verifying algorithms in Coq: an introduction

CEA-EDF-INRIA summer school, Paris, 7-11 June 2010.

Speakers: Yves Bertot, Pierre Casteran, Pierre Letouzey, Assia Mahboubi.

Assistants: Stéphane Glondu, Francesco Zappa Nardelli.

The Coq Proof Assistant can be downloaded from here. The files of these lectures have been tested with version 8.2pl1 but should work with any 8.2 (or 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.

Venue: Rooms Orange 1 and Orange 2 (5th floor), INRIA Antenne de Paris, 23 avenue d'Italie, 75013 Paris. Metro: Place d'Italie. Access plan.

Lecture 1 (Bertot): slides, sources, exercices.

Lecture 2 (Letouzey): slides, sources, exercices, solutions.

Lecture 3 (Casteran): slides, sources (and Tools.v - compile it by running coqc Tools), exercices.

Lecture 4 (Bertot): slides, exercices.

Lecture 5 (Bertot): slides, exercices, solutions.

Lecture 6 (Mahboubi): slides, exercices, solutions.

Lecture 7 (Mahboubi): slides, exercices, solutions.

Lecture 8 (Bertot): slides, sources, exercices, solutions.

Lecture 9 (Letouzey): slides, sources, exercices, solutions.

Lecture 10 (Casteran): slides, sources, exercices (again, do not forget to run coqc Tools), solutions.

All the files above in a .tar.gz archive.

Bonus exercise: certify a compiler for a simple arithmetic language (and its solution).

Schedule: lectures 9am-10.30am and 11am-12.30am, exercices 2pm-5.30pm.

Lunch: 12.30pm - 2pm, at the restaurant Via Italia, 21 avenue d'Italie.

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.


Email: Francesco.Zappa_Nardelli (at)

Address: Francesco Zappa Nardelli, Projet Moscova, INRIA Paris-Rocquencourt, Domaine de Voluceau, B.P. 105, 78153 Le Chesnay Cedex, France

Last updated: June 11, 2010.