===== Programmation et Preuves Formelles (Master 2 LMFI) =====

**Attention, ce cours est maintenant assuré par Alexis Saurin. La page ci-dessous concerne l'ancienne version du cours.**

=== Séances de pré-rentrée : initiation à la programmation en OCaml ===

Les [[https://gitlab.math.univ-paris-diderot.fr/letouzey/prog-lmfi/blob/master/ocaml/init-prog-ocaml.md|notes de cours]].

=== Cours de Coq : Programmation fonctionnelle et Preuves formelles ===

Mercredi 13h45-18h00 en salle 2018 (cours) puis 2006 (TP). Début le 14 septembre 2022, fin en décembre.
**Attention, ni cours ni TP le 2 novembre, remplacé par une dernière séance le 7 décembre**.

Partie I : programmation fonctionnelle en Coq, [[https://gitlab.math.univ-paris-diderot.fr/letouzey/coq-lmfi/tree/master/1-prog|Notes de cours et sujets de TD]].

Partie II : preuves formelles en Coq, [[https://gitlab.math.univ-paris-diderot.fr/letouzey/coq-lmfi/tree/master/2-preuves|Notes de cours et sujets de TD]].

== Projet ==

Date limite : **1er février 2023**.

Au choix, un des sujets suivants, ou bien votre proposition personnalisée (me contacter pour accord d'ici la fin du cours):

  * [[https://gitlab.math.univ-paris-diderot.fr/letouzey/coq-lmfi/blob/master/projet/projet-lzw|Compression LZW]]
  * [[https://gitlab.math.univ-paris-diderot.fr/letouzey/coq-lmfi/blob/master/projet/projet-compilo|Mini-compilateur certifié]].
  * [[https://gitlab.math.univ-paris-diderot.fr/letouzey/coq-lmfi/blob/master/projet/projet-heyting|Cohérence relative de l'arithmétique de Heyting]]
  * [[https://gitlab.math.univ-paris-diderot.fr/letouzey/coq-lmfi/tree/master/projet/projet-brzozowski|Expressions régulières et finitude des dérivées de Brzozowski]]
  * [[https://gitlab.math.univ-paris-diderot.fr/letouzey/coq-lmfi/tree/master/projet/projet-power-in-peano|Encodage de la fonction puissance en arithmétique de Peano]]

== Démo d'autres assistants de preuves ==

  * **Agda** : [[https://gitlab.math.univ-paris-diderot.fr/letouzey/cours-preuves/raw/master/m2lmfi/agda/Demo.agda|Demo.agda]] et [[https://gitlab.math.univ-paris-diderot.fr/letouzey/cours-preuves/raw/master/m2lmfi/agda/TypeDep.agda|TypDep.agda]]
  * **Hol Light** : [[http://www.cl.cam.ac.uk/~jrh13/papers/hollight.pdf|article]] de présentation, [[http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf|tutoriel]], et fichier [[https://gitlab.math.univ-paris-diderot.fr/letouzey/cours-preuves/raw/master/m2lmfi/hol-light/demo.ml|demo.ml]]
  * **Isabelle** : [[http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf|article]] et fichiers de demo [[https://gitlab.math.univ-paris-diderot.fr/letouzey/cours-preuves/raw/master/m2lmfi/isabelle/IFOLBIS.thy|IFOLBIS.thy]] et [[https://gitlab.math.univ-paris-diderot.fr/letouzey/cours-preuves/raw/master/m2lmfi/isabelle/ToyList.thy|ToyList.thy]]

=== Ancien cours de programmation en OCaml ===

[[.:proglmfi-ocaml|cours de 2015-2017]] (en OCaml).