Translating HOL to Dedukti

Ali Assaf
(Inria, Ecole Polytechnique) 		Guillaume Burel
(ENSIIE/Cédric)

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.

In Cezary Kaliszyk and Andrei Paskevich: Proceedings Fourth Workshop on Proof eXchange for Theorem Proving (PxTP 2015), Berlin, Germany, August 2-3, 2015, Electronic Proceedings in Theoretical Computer Science 186, pp. 74–88.
Published: 30th July 2015.
ArXived at: https://dx.doi.org/10.4204/EPTCS.186.8 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org