## Modelling and verifying algorithms in Coq: an introduction

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.

For any question, please contact

*Francesco.Zappa_Nardelli (at) inria.fr*

Last updated:

*November 18, 2011*.