Document Open Access Logo

Virtualization of HOL4 in Isabelle

Authors Fabian Immler , Jonas Rädle , Makarius Wenzel

PDF

File

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

Document Identifiers

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
    0
    Metadata Views

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.

Cite As Get 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

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

Funding

  • Immler, Fabian: This material is based upon work supported by the Air Force Office of Scientific Research under grant number FA9550-18-1-0120. Any opinions, finding, and conclusion or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the United States Air Force.

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.

Supplementary Materials

References

  1. Andrew W Appel, James S Mattson, and David Tarditi. A lexical analyzer generator for Standard ML. Distributed with Standard ML of New Jersey, 1989. Google Scholar
  2. Andrej Bauer, Martín Escardó, Peter L. Lumsdaine, and Assia Mahboubi. Formalization of Mathematics in Type Theory (Dagstuhl Seminar 18341). Dagstuhl Reports, 8(8):130-155, 2019. URL: https://doi.org/10.4230/DagRep.8.8.130.
  3. Manuel Eberl, Gerwin Klein, Tobias Nipkow, Larry Paulson, and René Thiemann (editors). The Archive of Formal Proofs. Online Journal. URL: https://www.isa-afp.org.
  4. M. J. C. Gordon, R. Milner, and C. P. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer, 1979. Google Scholar
  5. Brian Huffman and Ondřej Kunčar. Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL. In Georges Gonthier and Michael Norrish, editors, Certified Programs and Proofs, pages 131-146, Cham, 2013. Springer International Publishing. Google Scholar
  6. Lars Hupel. Splicing runtime ML values into Isar. isabelle-users mailing list. 09 Jun 2015, URL: https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-June/msg00076.html.
  7. Lars Hupel. CakeML. Archive of Formal Proofs, 2018, 2018. URL: https://www.isa-afp.org/entries/CakeML.html.
  8. J. Hurd. OpenTheory: Package Management for Higher Order Logic Theories. In G. Dos Reis and L. Théry, editors, Programming Languages for Mechanized Mathematics Systems, pages 31-37. ACM, 2009. Google Scholar
  9. Joe Hurd. The OpenTheory Standard Theory Library. In Mihaela Gheorghiu Bobaru, Klaus Havelund, Gerard J. Holzmann, and Rajeev Joshi, editors, NASA Formal Methods - Third International Symposium, NFM 2011, Pasadena, CA, USA, April 18-20, 2011. Proceedings, volume 6617 of Lecture Notes in Computer Science, pages 177-191. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-20398-5.
  10. Cezary Kaliszyk and Alexander Krauss. Scalable LCF-Style Proof Translation. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving, pages 51-66, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
  11. Chantal Keller and Benjamin Werner. Importing HOL Light into Coq. In Matt Kaufmann and Lawrence C. Paulson, editors, Interactive Theorem Proving, pages 307-322, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. Google Scholar
  12. Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. CakeML: a verified implementation of ML. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 179-192, 2014. URL: https://doi.org/10.1145/2535838.2535841.
  13. Ondřej Kunčar. Types, Abstraction and Parametric Polymorphism in Higher-Order Logic. Dissertation, Technische Universität München, München, 2016. URL: http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:bvb:91-diss-20160408-1285267-1-5.
  14. David Matthews. The Poly/ML implementation of Standard ML. Website. URL: https://www.polyml.org.
  15. Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. Isabelle/HOL: a proof assistant for higher-order logic, volume 2283. Springer Science & Business Media, 2002. Google Scholar
  16. Steven Obua and Sebastian Skalberg. Importing HOL into Isabelle/HOL. In Ulrich Furbach and Natarajan Shankar, editors, Automated Reasoning, pages 298-302, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. Google Scholar
  17. Lawrence C Paulson. Isabelle: A generic theorem prover, volume 828. Springer Science & Business Media, 1994. Google Scholar
  18. Konrad Slind. Function definition in higher-order logic. In Gerhard Goos, Juris Hartmanis, Jan van Leeuwen, Joakim von Wright, Jim Grundy, and John Harrison, editors, Theorem Proving in Higher Order Logics, pages 381-397, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg. Google Scholar
  19. Konrad Slind and Michael Norrish. A brief overview of HOL4. In International Conference on Theorem Proving in Higher Order Logics, pages 28-32. Springer, 2008. Google Scholar
  20. Makarius Wenzel. Asynchronous User Interaction and Tool Integration in Isabelle/PIDE. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving - 5th International Conference, ITP 2014, Vienna, Austria, volume 8558 of Lecture Notes in Computer Science. Springer, 2014. URL: https://www21.in.tum.de/~wenzelm/papers/itp-pide.pdf.
  21. Makarius Wenzel. The Isabelle/Isar Implementation, 2019. URL: http://isabelle.in.tum.de/website-Isabelle2019/dist/Isabelle2019/doc/implementation.pdf.
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
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact