Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH scholarly article en Immler, Fabian; Rädle, Jonas; Wenzel, Makarius License: Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)
when quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-110760

; ;

Virtualization of HOL4 in Isabelle



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

  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 =		{},
  URN =		{urn:nbn:de:0030-drops-110760},
  doi =		{10.4230/LIPIcs.ITP.2019.21},
  annote =	{Keywords: Virtualization, HOL4, Isabelle, Isabelle/HOL, Isabelle/ML}

Keywords: Virtualization, HOL4, Isabelle, Isabelle/HOL, Isabelle/ML
Seminar: 10th International Conference on Interactive Theorem Proving (ITP 2019)
Issue date: 2019
Date of publication: 05.09.2019
Supplementary Material: Our implementation is available online, it works with Isabelle2019 and the following development version of the official HOL4 repository.

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI