Outil de traduction automatique permettant de convertir des fichiers au format Rec vers le format Dedukti. Ce projet facilite l'interopérabilité entre différents systèmes de preuve formelle, notamment pour la vérification de théorèmes en logique mathématique. Il s'adresse principalement aux chercheurs et développeurs travaillant dans le domaine de la démonstration automatique et de la logique formelle.

Ce projet propose une traduction automatique d'une partie de la bibliothèque HOL-Light vers le système Rocq. Il permet d'aligner des types et fonctions mathématiques entre ces deux environnements de preuve formelle, facilitant ainsi l'utilisation de théorèmes HOL-Light dans Rocq. L'objectif est d'accélérer le développement de preuves formelles en exploitant des résultats déjà établis dans HOL-Light, tout en garantissant leur compatibilité avec Rocq.

Outil dédié à la traduction générique de théories dans le langage Dedukti, un système basé sur le λΠ-calcul modulo théorie. Il propose trois modèles de traduction : les morphismes de théorie, les relations logiques et les plongements de théorie. Ces fonctionnalités aident les utilisateurs à adapter des systèmes formels entre eux, facilitant ainsi la réutilisation et l'interopérabilité des preuves logiques.

Ce projet propose une bibliothèque Rocq (anciennement Coq) qui automatise la traduction d'une partie de la bibliothèque HOL-Light en utilisant des outils dédiés. Il permet de mapper des types et fonctions de HOL-Light vers des constructions idiomatiques dans Rocq, facilitant ainsi l'interopérabilité entre ces deux systèmes de preuve formelle. Les théorèmes traduits sont fournis comme axiomes pour optimiser les performances.

Ce projet propose une bibliothèque Rocq (anciennement Coq) qui automatise la traduction d'une partie de la bibliothèque HOL-Light dédiée à la logique. L'objectif est de permettre une utilisation idiomatique des types et fonctions de HOL-Light dans Rocq, facilitant ainsi l'interopérabilité entre ces deux systèmes de preuve formelle. Les théorèmes traduits sont fournis sous forme d'axiomes pour optimiser les performances.

Ce projet propose une bibliothèque Rocq qui automatise la traduction des bibliothèques HOL-Light vers Rocq, permettant d'utiliser des théorèmes et fonctions mathématiques dans Rocq. Il facilite l'interopérabilité entre ces deux systèmes de preuve formelle en alignant types et fonctions, et offre un accès à plus de 20 000 théorèmes couvrant des domaines variés comme l'arithmétique, l'algèbre, l'analyse ou la topologie. Les preuves traduites sont fournies sous forme d'axiomes pour une utilisation rapide, avec la possibilité de régénérer et vérifier les preuves originales si nécessaire.

Ce projet propose une traduction de la bibliothèque arithmétique de Matita vers le langage Agda. Il facilite l'échange et la vérification de preuves mathématiques entre différents systèmes formels. L'objectif est d'améliorer l'interopérabilité et la réutilisation des travaux en logique et en mathématiques formelles.