===== Outline of the course Functional programming and formal proofs in Coq =====

==== Course outline ====

The Coq files corresponding to the course as well as addition material will be gathered on [[https://gitlab.math.univ-paris-diderot.fr/saurin/coq-lmfi-2023|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!
    * [[https://www.irif.fr/users/saurin/teaching/lmfi/coq-2023/tp0|webpage presenting TP0]]
    * [[https://gitlab.math.univ-paris-diderot.fr/saurin/coq-lmfi-2023/-/blob/main/TP/TP0.v|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?)