The Coq files corresponding to the course as well as addition material will be gathered on this git repository from which you can download them.
TP0: First steps… Open the webpage for TP0, download the file TP0.v and follow the instructions!
Lecture 1 (27/09): prog 1 – Prise en main, base sur les types de Coq et introduction aux types inductifs et à la récursion.
Lecture 2 (4/10): prog 2 – Plus de types inductifs
Lecture 3 (11/10): prog 3 – Principes d'induction et de pseudo induction, introduction aux types dépendants
Lecture 4 (18/10): prog 4 – Types dépendants
Lecture 5 (25/10): preuves 1 – ??? (attention, décalage à cause de la visite HCERES.)
Lecture 6 (08/11) : preuves 2 – ???
Lecture 7 (15/11) : preuves 3 – ???
Lecture 8 (22/11) : preuves 4 – ???
Lecture 9 (29/11) : prog 5 – Monades, modules, records et extraction
Lecture 10 (06/12) : preuves 5 – ???
Lecture 11 (13/12) : preuves 6 – ???
Lecture 12 (20/12) : preuves 7 – ??? (attention, semaine d'examen: soit en janvier, soit en rattrapant une séance au moins de novembre ou début décembre, ou en débutant les cours à 14H si salle dispo?)