The Common HOL Platform
Mark Adams (Proof Technologies Ltd, UK, Radboud University,, Nijmegen, The Netherlands)
TL;DR
The paper introduces the Common HOL Platform, a standard API and theory for HOL theorem provers, enabling easier porting of code and proofs across different systems, demonstrated through successful code translation.
Contribution
It presents the design and implementation of the Common HOL Platform, facilitating interoperability among HOL theorem provers and demonstrating its practical application.
Findings
Successful adaptation of HOL Light and hol90 to the platform
Effective translation of source code from HOL Light to HOL Zero
Enhanced compatibility among HOL systems
Abstract
The Common HOL project aims to facilitate porting source code and proofs between members of the HOL family of theorem provers. At the heart of the project is the Common HOL Platform, which defines a standard HOL theory and API that aims to be compatible with all HOL systems. So far, HOL Light and hol90 have been adapted for conformance, and HOL Zero was originally developed to conform. In this paper we provide motivation for a platform, give an overview of the Common HOL Platform's theory and API components, and show how to adapt legacy systems. We also report on the platform's successful application in the hand-translation of a few thousand lines of source code from HOL Light to HOL Zero.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.