Coq est un système de gestion de preuves formelles. Il fournit un langage formel pour écrire des définitions mathématiques, des algorithmes exécutables et des théorèmes, ainsi qu'un environnement pour le développement semi-interactif de preuves formelles vérifiables par machine.

Opam est un gestionnaire de paquets source pour le langage de programmation OCaml. Il supporte plusieurs installations de compilateurs simultanées, des contraintes flexibles de paquets et un workflow de développement Git-friendly.

Caradoc est un outil d'analyse, de validation et d'extraction de données pour les fichiers PDF. Il est écrit en OCaml et fournit de nombreuses commandes pour analyser les PDF, ainsi qu'une interface utilisateur en console.

La plateforme Coq est une distribution du logiciel Coq, un assistant de preuve pour les mathématiques, accompagnée d'une sélection de bibliothèques et de plugins. Elle vise à être indépendante du système d'exploitation, fiable, facile à installer et complète.

Zelus est un langage synchrone étendu avec des équations différentielles ordinaires (ODE) pour programmer des systèmes hybrides qui mélangent des modèles discrets et continus. Il partage les principes de base des langages synchrones Lustre et Lucid Synchrone, avec des fonctionnalités supplémentaires telles que la déduction de types, les automates hiérarchiques et les fonctions d'ordre supérieur.

MPP est un préprocesseur et un méta-préprocesseur simple et personnalisable, qui permet de définir des variables et d'utiliser des conditions dans les fichiers de code source, en utilisant des tokens définissables par l'utilisateur.

Obi est un dépôt contenant les scripts, les bibliothèques et les outils en ligne de commande nécessaires pour accéder à l'infrastructure de construction en vrac qui vérifie la santé du gestionnaire de paquets OCaml, opam.

Clangml est une interface écrite en OCaml permettant d'analyser et de générer des informations à partir de code source C en utilisant Clang.

Ce bot, écrit en OCaml, est principalement utilisé dans le développement du projet Coq. Il permet la synchronisation entre GitHub et GitLab, la gestion des pull requests depuis des forks, la gestion des milestones des issues et la gestion du processus de backporting.

Ce projet est un dépôt de code source pour le cours UE LIFPF INF2030L Programmation Fonctionnelle du semestre 2024 Printemps. Il contient des diapositives, des sujets de TD, de TP et de CM, ainsi que des corrigés et des configurations pour les salles de TP. Les thèmes abordés dans ce cours sont le lambda-calcul, le langage de programmation OCaml, les structures de données récursives, les foncteurs, et l'ordre supérieur.