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 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, Notes de cours et sujets de TD. Partie II : preuves formelles en Coq, 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): Compression LZW Mini-compilateur certifié. Cohérence relative de l'arithmétique de Heyting Expressions régulières et finitude des dérivées de Brzozowski Encodage de la fonction puissance en arithmétique de Peano Démo d'autres assistants de preuves Agda : Demo.agda et TypDep.agda Hol Light : article de présentation, tutoriel, et fichier demo.ml Isabelle : article et fichiers de demo IFOLBIS.thy et ToyList.thy Ancien cours de programmation en OCaml cours de 2015-2017 (en OCaml).