Ce projet académique propose un enseignement complet en programmation fonctionnelle et en preuves formelles utilisant l'assistant de preuve Coq/Rocq. Destiné aux étudiants de Master 2 LMFI de l'Université de Paris, il couvre des sujets avancés comme la compression de données, la compilation certifiée et la formalisation de théorèmes mathématiques. Les étudiants réalisent des projets pratiques pour appliquer ces concepts théoriques.