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.

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 (anciennement Coq) qui traduit automatiquement la bibliothèque HOL-Light dédiée à la logique. Il permet de manipuler des types et fonctions idiomatiques en Rocq tout en conservant les propriétés et théorèmes originaux. L'objectif est de faciliter l'interopérabilité entre ces deux environnements de preuve formelle pour des applications en vérification mathématique et en intelligence artificielle.

Ce projet développe une bibliothèque Rocq qui traduit automatiquement une partie de la bibliothèque HOL-Light, notamment la définition des nombres réels et des fonctions associées, vers des types et fonctions compatibles avec MathComp. L'objectif est de permettre l'utilisation de théorèmes HOL-Light dans des développements Rocq, facilitant ainsi l'interopérabilité entre ces environnements de preuve formelle. Les preuves traduites sont fournies comme axiomes pour une intégration rapide, tout en restant vérifiables via un script dédié.

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 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.