CoqInTheClassroomInitial

Teaching Coq (first experiences in France)

First experiences in Paris and Lyon

From the late 80's, a class on proofs, types and formalisation was held at Paris with Gérard Huet and Thierry Coquand as teachers, then with Gilles Dowek. Christine Paulin taught a class Types et Preuves (Types and Proofs) at ENS Lyon from 1992 to 1996.

Benjamin Werner taught Coq at the master level of the French ENSTA Engineer Advanced School as soon as 1996. This was using Coq version 6.2 beta and the class was entitled Preuves sur ordinateur (Proof on computers).

Coq has been taught more deeply in the context of the second-year-of-master-level DEA of Programmation in Paris from 1997 by Christine Paulin and Benjamin Werner. The DEA course focused both on the foundations and applications of Coq. After the Licence-Master-PhD standardisation at the European level, the DEA got renamed Master. The class didn't evolved much and the original notes by Christine Paulin and Benjamin Werner, enriched from new chapters by Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin and Claude Marché, are still used and available online.

Other experiences in France

Loïc Pottier and Laurent Théry used Coq (and the graphical interface CtCoq) in a class on Proofs of Algorithms (at least in 1998 and 1999).

Experiences were made at the first year of the Master level at ENS Lyon by Yves Bertot (from 2002). This class id now taught by Jean Duprat.

From 2004, Alexandre Miquel taught Coq at the first year of the master level at University Paris 7. He has exercises and a "guide de survie" for a class at the second year of the master level (in French).

Nicolas Magaud and Julien Narboux have a class Ingénierie de la preuve at the University of Strasbourg.

Jean François Dufourd has a class Spécifications formelles, preuves et programmation at the University of Strasbourg.