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.

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.

Zenon Modulo est un solveur de preuves automatisé pour la logique du premier ordre classique avec types polymorphes. Il accepte les fichiers d'entrée avec la syntaxe TPTP (FOF et TFF1) et Dedukti. Il peut produire des certificats de preuve pour Dedukti. Il est utilisé dans les projets FoCaLiZe et BWare.

CoqInE est un plugin pour le logiciel Coq qui traduit les preuves Coq en termes Dedukti vérifiables. Il fournit un fichier de signature fidèlement encodant la théorie sous-jacente de Coq. La sortie générée est destinée à être vérifiable à l'aide de la dernière version de Dedukti.

Ce programme vérifie la terminaison d'autres programmes en utilisant le critère de terminaison Size-Change. Il accepte en entrée des fichiers Dedukti ou des fichiers XML de la Termination Problem Data Base.

Holide est un traducteur de fichiers de théories formelles de HOL vers Dedukti. Il permet de vérifier la validité des théories formelles dans le langage Dedukti.

CDUCE est un langage de programmation adapté à la manipulation de documents XML. Il a été conçu et développé dans le cadre d'un projet de recherche conjoint entre le groupe Langages de l'ENS (Paris) et le groupe Base de données du LRI (Orsay). L'implémentation actuelle a été écrite pour démontrer les fonctionnalités innovantes du langage et valider les choix de conception. Il s'agit d'un prototype de recherche, pas d'une application robuste. Cependant, il a été signalé qu'il fonctionne correctement dans un environnement de production.

Ekstrakto est un outil permettant de traduire des preuves au format TSTP en preuves lambdapi. Il génère des fichiers TPTP pour chaque étape de la preuve TSTP, ainsi qu'un fichier de signature lambdapi et un fichier de preuve lambdapi complet. Il peut ensuite être utilisé avec des preuves automatisées pour générer des fichiers de preuve lambdapi pour chaque étape.

STTfaXport est un outil permettant d'exporter des théories écrites dans le langage de déduction Dedukti vers d'autres assistants de preuve en utilisant l'encodage de STTfa. Il nécessite OCaml, Dedukti et dune pour fonctionner.

Ce projet est un compilateur qui prend en entrée des fichiers écrits dans un langage spécifique et génère du code source dans un autre langage. Il effectue l'analyse syntaxique et sémantique du code source, ainsi que des optimisations pour améliorer les performances du code généré.