CEA-EDF-INRIA summer school, Paris, 7-11 June 2010.
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.
All the files above in a .tar.gz archive.
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) inria.fr
Address: Francesco Zappa Nardelli, Projet Moscova, INRIA Paris-Rocquencourt, Domaine de Voluceau, B.P. 105, 78153 Le Chesnay Cedex, France