LIPIcs.ITP.2019.21.pdf
- Filesize: 0.64 MB
- 18 pages
Document
Virtualization of HOL4 in Isabelle
Authors
Fabian Immler 
,
Jonas Rädle ,
-
Part of:
Volume:
10th International Conference on Interactive Theorem Proving (ITP 2019)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 3.0 Unported license
- Publication date: 2019-09-05
File
Document Identifiers
Author Details
Acknowledgements
Dagstuhl Seminar 18341 Formalization of Mathematics in Type Theory [Andrej Bauer et al., 2019] hosted the working group "Interoperability of systems" (by Mario Carneiro), which provided an excellent environment to discuss early experiments and helped to structure this approach. We thank the HOL4 team (especially Michael Norrish) for support and accepting changes to HOL4.
Cite AsGet BibTex
Fabian Immler, Jonas Rädle, and Makarius Wenzel. Virtualization of HOL4 in Isabelle. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 21:1-21:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ITP.2019.21
https://doi.org/10.4230/LIPIcs.ITP.2019.21
Abstract
We present a novel approach to combine the HOL4 and Isabelle theorem provers: both are implemented in SML and based on distinctive variants of HOL. The design of HOL4 allows to replace its inference kernel modules, and the system infrastructure of Isabelle allows to embed other applications of SML. That is the starting point to provide a virtual instance of HOL4 in the same run-time environment as Isabelle. Moreover, with an implementation of a virtual HOL4 kernel that operates on Isabelle/HOL terms and theorems, we can load substantial HOL4 libraries to make them Isabelle theories, but still disconnected from existing Isabelle content. Finally, we introduce a methodology based on the transfer package of Isabelle to connect the imported HOL4 material to that of Isabelle/HOL.
Subject Classification
ACM Subject Classification
- Software and its engineering → Interoperability
- Theory of computation → Higher order logic
Keywords
- Virtualization
- HOL4
- Isabelle
- Isabelle/HOL
- Isabelle/ML
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads