Traduction de HOL en Dedukti
Résumé
Les systèmes de preuve actuels (Coq, HOL, PVS, etc.) sont très utiles pour le développement des mathématiques et la vérification de programmes. Cependant, ils souffrent d'un manque d'interopérabilité qui rend difficile la réutilisation des preuves. Dedukti est un système de preuve universel basé sur le λΠ-calcul modulo qui peut exprimer des preuves venant de systèmes différents. Burel et Boespflug ont déjà travaillé sur une traduction de Coq en Dedukti. L'objectif de ce stage était de concevoir une traduction de HOL vers Dedukti. Le stage a abouti à une expression de HOL dans le λΠ-calcul modulo, ainsi qu'à un programme de traduction automatique des preuves de HOL, écrites dans le standard OpenTheory, vers Dedukti. Une partie simplifiée de l'encodage est prouvée comme étant correcte et complète. Le programme de traduction génère des fichiers qui sont vérifiés et validés par Dedukti. L'ensemble de HOL et de sa bibliothèque standard est traduit et vérifié dans Dedukti. C'est une nouvelle étape pour une meilleure interopérabilité entre les systèmes de preuve.
Domaines
Logique en informatique [cs.LO]
Origine : Fichiers produits par l'(les) auteur(s)
Loading...