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!
  • webpage presenting TP0
  • visit this page to download TP0.v
• 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?)