License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2019.21
URN: urn:nbn:de:0030-drops-110760
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11076/
Immler, Fabian ;
Rädle, Jonas ;
Wenzel, Makarius
Virtualization of HOL4 in Isabelle
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.
BibTeX - Entry
@InProceedings{immler_et_al:LIPIcs:2019:11076,
author = {Fabian Immler and Jonas R{\"a}dle and Makarius Wenzel},
title = {{Virtualization of HOL4 in Isabelle}},
booktitle = {10th International Conference on Interactive Theorem Proving (ITP 2019)},
pages = {21:1--21:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-122-1},
ISSN = {1868-8969},
year = {2019},
volume = {141},
editor = {John Harrison and John O'Leary and Andrew Tolmach},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2019/11076},
URN = {urn:nbn:de:0030-drops-110760},
doi = {10.4230/LIPIcs.ITP.2019.21},
annote = {Keywords: Virtualization, HOL4, Isabelle, Isabelle/HOL, Isabelle/ML}
}
