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: RoomsOrange 1andOrange 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 runningcoqc 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 runcoqc Tools), solutions.All the files above in a

.tar.gzarchive.

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

Contact:

*Email:* Francesco.Zappa_Nardelli (at) inria.fr

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

Last updated: