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 https://www.dagstuhl.de/lipics License: Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-110760
URL:

; ;

Virtualization of HOL4 in Isabelle

pdf-format:


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}
}

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. https://github.com/immler/hol4isabelle https://isabelle.in.tum.de/website-Isabelle2019 https://github.com/HOL-Theorem-Prover/HOL/commit/7e03303e51f


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