Translating HOL to Dedukti

Abstract : Dedukti is a logical framework based on the λΠ-calculus modulo rewriting, which extends the λΠ-calculus with rewrite rules. In this paper, we show how to translate the proofs of a family of HOL proof assistants to Dedukti. The translation preserves binding, typing, and reduction. We implemented this translation in an automated tool and used it to successfully translate the OpenTheory standard library.
Type de document :
Communication dans un congrès
Cezary Kaliszyk; Andrei Paskevich. Fourth Workshop on Proof eXchange for Theorem Proving, PxTP'15, Aug 2015, Berlin, Germany. 186, pp.74-88, 2015, EPTCS. 〈http://pxtp15.lri.fr/〉. 〈10.4204/EPTCS.186.8〉
Liste complète des métadonnées

Littérature citée [29 références]  Voir  Masquer  Télécharger

https://hal.archives-ouvertes.fr/hal-01097412
Contributeur : Guillaume Burel <>
Soumis le : vendredi 18 décembre 2015 - 15:25:48
Dernière modification le : mardi 22 décembre 2015 - 01:04:38
Document(s) archivé(s) le : samedi 19 mars 2016 - 10:31:30

Fichier

translating-hollight-dedukti-p...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Collections

Citation

Ali Assaf, Guillaume Burel. Translating HOL to Dedukti. Cezary Kaliszyk; Andrei Paskevich. Fourth Workshop on Proof eXchange for Theorem Proving, PxTP'15, Aug 2015, Berlin, Germany. 186, pp.74-88, 2015, EPTCS. 〈http://pxtp15.lri.fr/〉. 〈10.4204/EPTCS.186.8〉. 〈hal-01097412v2〉

Partager

Métriques

Consultations de la notice

181

Téléchargements de fichiers

125