Translating HOL to Dedukti
Ali Assaf (Inria, Ecole Polytechnique), Guillaume Burel, (ENSIIE/C\'edric)
TL;DR
This paper presents an automated translation method from HOL proof assistants to Dedukti, preserving logical properties and enabling interoperability, demonstrated by translating the OpenTheory library.
Contribution
It introduces a novel translation technique from HOL to Dedukti, implemented as an automated tool, facilitating proof interoperability and reuse.
Findings
Successfully translated OpenTheory library proofs to Dedukti
Preserved binding, typing, and reduction during translation
Automated the translation process for practical use
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.