|
 
|
[AB15] Translating HOL to Dedukti
Conférence Internationale avec comité de lecture : Fourth Workshop on Proof eXchange for Theorem Proving, August 2015, pp.--, Series EPTCS, Berlin, Germany,Mots clés: higher-order logic; lambda-Pi calculus modulo rewriting; logical framework; dependent types
Résumé:
Dedukti is a logical framework based on the lambda-Pi calculus modulo rewriting, which extends the lambda-Pi 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.
Equipe:
sys
Collaboration:
INRIA
BibTeX
| @inproceedings { | |||
| AB15, | |||
| title | = | "{Translating HOL to Dedukti}", | |
| author | = | " A. Assaf and G. Burel ", | |
| booktitle | = | "{Fourth Workshop on Proof eXchange for Theorem Proving}", | |
| year | = | 2015, | |
| month | = | "August", | |
| series | = | "EPTCS", | |
| pages | = | "--", | |
| address | = | "Berlin, Germany", | |
| } | |||
