Skip to Main content Skip to Navigation
Master thesis

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.
Document type :
Master thesis
Complete list of metadata

Cited literature [20 references]  Display  Hide  Download

https://hal.inria.fr/hal-00919871
Contributor : Ali Assaf <>
Submitted on : Tuesday, December 17, 2013 - 2:08:41 PM
Last modification on : Friday, May 25, 2018 - 12:02:06 PM
Long-term archiving on: : Monday, March 17, 2014 - 11:16:16 PM

Files

rapport.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00919871, version 1

Collections

Citation

Ali Assaf. Traduction de HOL en Dedukti. Logique en informatique [cs.LO]. 2012. ⟨hal-00919871⟩

Share

Metrics

Record views

245

Files downloads

216