Document Open Access Logo

Virtualization of HOL4 in Isabelle

Authors Fabian Immler , Jonas Rädle , Makarius Wenzel



PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.21.pdf
  • Filesize: 0.64 MB
  • 18 pages

Document Identifiers

Author Details

Fabian Immler
  • School of Computer Science, Carnegie Mellon University, USA
Jonas Rädle
  • Fakultät für Informatik, Technische Universität München, Germany
Makarius Wenzel
  • Augsburg, Germany

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

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)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail