Candle: A Verified Implementation of HOL Light
View / Open Files
Publication Date
2022-08-03Journal Title
13th International Conference on Interactive Theorem Proving (ITP 2022)
Conference Name
Thirteenth Conference on Interactive Theorem Proving
ISSN
1868-8969
ISBN
978-3-95977-252-5
Publisher
Schloss Dagstuhl -- Leibniz-Zentrum fur Informatik
Type
Conference Object
This Version
VoR
Metadata
Show full item recordCitation
Abrahamsson, O., Myreen, M. O., Kumar, R., & Sewell, T. (2022). Candle: A Verified Implementation of HOL Light. 13th International Conference on Interactive Theorem Proving (ITP 2022) https://doi.org/10.4230/LIPIcs.ITP.2022.3
Abstract
This paper presents a fully verified interactive theorem prover for higher-order logic, more specifically:
a fully verified clone of HOL Light. Our verification proof of this new system results in an end-to-end
correctness theorem that guarantees the soundness of the entire system down to the machine code
that executes at runtime. Our theorem states that every exported fact produced by this machine-code
program is valid in higher-order logic. Our implementation consists of a read-eval-print loop (REPL)
that executes the CakeML compiler internally. Throughout this work, we have strived to make the
REPL of the new system provide a user experience as close to HOL Light’s as possible. To this end,
we have, e.g., made the new system parse the same variant of OCaml syntax as HOL Light. All of
the work described in this paper has been carried out in the HOL4 theorem prover.
Identifiers
External DOI: https://doi.org/10.4230/LIPIcs.ITP.2022.3
This record's URL: https://www.repository.cam.ac.uk/handle/1810/336698
Statistics
Total file downloads (since January 2020). For more information on metrics see the
IRUS guide.
Recommended or similar items
The current recommendation prototype on the Apollo Repository will be turned off on 03 February 2023. Although the pilot has been fruitful for both parties, the service provider IKVA is focusing on horizon scanning products and so the recommender service can no longer be supported. We recognise the importance of recommender services in supporting research discovery and are evaluating offerings from other service providers. If you would like to offer feedback on this decision please contact us on: support@repository.cam.ac.uk