{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T08:54:22Z","timestamp":1766134462356,"version":"3.48.0"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2025,12,1]],"date-time":"2025-12-01T00:00:00Z","timestamp":1764547200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,12,5]],"date-time":"2025-12-05T00:00:00Z","timestamp":1764892800000},"content-version":"vor","delay-in-days":4,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100005760","name":"University of Gothenburg","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100005760","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>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\u2019s 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.<\/jats:p>","DOI":"10.1007\/s10817-025-09743-8","type":"journal-article","created":{"date-parts":[[2025,12,5]],"date-time":"2025-12-05T09:33:34Z","timestamp":1764927214000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Candle: A Verified Implementation of HOL\u00a0Light (Extended Version)"],"prefix":"10.1007","volume":"69","author":[{"given":"Oskar","family":"Abrahamsson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Magnus O.","family":"Myreen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ramana","family":"Kumar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Sewell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,12,5]]},"reference":[{"key":"9743_CR1","doi-asserted-by":"publisher","unstructured":"Myreen, M.O., Davis, J.: A verified runtime for a verified theorem prover. (eds van Eekelen, M. C. J.\u00a0D., Geuvers, H., Schmaltz, J. & Wiedijk, F.) Interactive Theorem Proving (ITP), Vol. 6898 of LNCS (Springer, 2011). https:\/\/doi.org\/10.1007\/978-3-642-22863-6_20","DOI":"10.1007\/978-3-642-22863-6_20"},{"key":"9743_CR2","doi-asserted-by":"publisher","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. (eds Mohamed, O.\u00a0A., Mu\u00f1oz, C.\u00a0A. & Tahar, S.) Theorem Proving in Higher Order Logics (TPHOLs), Vol. 5170 of LNCS (Springer, 2008).https:\/\/doi.org\/10.1007\/978-3-540-71067-7_6","DOI":"10.1007\/978-3-540-71067-7_6"},{"key":"9743_CR3","doi-asserted-by":"publisher","unstructured":"Harrison, J.: HOL Light: An overview. (eds Berghofer, S., Nipkow, T., Urban, C. & Wenzel, M.) Theorem Proving in Higher Order Logics (TPHOLs), Vol. 5674 of Lecture Notes in Computer Science, 60\u201366 (Springer, 2009).https:\/\/doi.org\/10.1007\/978-3-642-03359-9_4","DOI":"10.1007\/978-3-642-03359-9_4"},{"key":"9743_CR4","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1007\/s00165-019-00492-1","volume":"31","author":"LC Paulson","year":"2019","unstructured":"Paulson, L.C., Nipkow, T., Wenzel, M.: From lcf to isabelle\/hol. Formal Aspects Comput. 31, 675\u2013698 (2019). https:\/\/doi.org\/10.1007\/s00165-019-00492-1","journal-title":"Formal Aspects Comput."},{"key":"9743_CR5","unstructured":"Arthan, R.: ProofPower (2008). https:\/\/www.lemma-one.com\/ProofPower\/index\/"},{"key":"9743_CR6","doi-asserted-by":"publisher","unstructured":"Abrahamsson, O., Myreen, M.O., Kumar, R., Sewell, T.: Candle: A verified implementation of HOL Light. (eds Andronick, J. & de\u00a0Moura, L.) Interactive Theorem Proving (ITP), Vol. 237 of LIPIcs (LIPIcs, 2022). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2022.3","DOI":"10.4230\/LIPIcs.ITP.2022.3"},{"key":"9743_CR7","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/s10817-025-09719-8","volume":"69","author":"O Abrahamsson","year":"2025","unstructured":"Abrahamsson, O., Myreen, M.O., Norrish, M., Kanabar, H., Pohjola, J.\u00c5.: Fast, verified computation for hol itps. J. Autom. Reason. 69, 7 (2025). https:\/\/doi.org\/10.1007\/s10817-025-09719-8","journal-title":"J. Autom. Reason."},{"key":"9743_CR8","doi-asserted-by":"publisher","unstructured":"Sewell, T. et\u00a0al.:Cakes that bake cakes: Dynamic computation in CakeML. (ed. Foster, N.) Programming Language Design and Implementation (PLDI) (ACM, 2023). https:\/\/doi.org\/10.1145\/3591266","DOI":"10.1145\/3591266"},{"key":"9743_CR9","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/s10817-015-9357-x","volume":"56","author":"R Kumar","year":"2016","unstructured":"Kumar, R., Arthan, R., Myreen, M.O., Owens, S.: Self-formalisation of higher-order logic - semantics, soundness, and a verified implementation. J. Autom. Reason. 56, 221\u2013259 (2016). https:\/\/doi.org\/10.1007\/s10817-015-9357-x","journal-title":"J. Autom. Reason."},{"key":"9743_CR10","doi-asserted-by":"publisher","unstructured":"Tan, Y.K. et\u00a0al.: The verified CakeML compiler backend. Journal of Functional Programming29 (2019). https:\/\/doi.org\/10.1017\/S0956796818000229","DOI":"10.1017\/S0956796818000229"},{"key":"9743_CR11","doi-asserted-by":"publisher","unstructured":"Tan, Y.\u00a0K., Owens, S., Kumar, R.: A verified type system for CakeML. (ed. L\u00e4mmel, R.) Implementation and Application of Functional Programming Languages (IFL) (ACM, 2015). https:\/\/doi.org\/10.1145\/2897336.2897344","DOI":"10.1145\/2897336.2897344"},{"key":"9743_CR12","doi-asserted-by":"publisher","unstructured":"Myreen, M.\u00a0O., Owens, S. Proof-producing translation of higher-order logic into pure and stateful ML. J. Funct. Program.24 (2014). https:\/\/doi.org\/10.1017\/S0956796813000282","DOI":"10.1017\/S0956796813000282"},{"key":"9743_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09559-8","author":"O Abrahamsson","year":"2020","unstructured":"Abrahamsson, O., et al.: Proof-producing synthesis of CakeML from monadic HOL functions. Journal of Automated Reasoning (JAR) (2020). https:\/\/doi.org\/10.1007\/s10817-020-09559-8","journal-title":"Journal of Automated Reasoning (JAR)"},{"key":"9743_CR14","doi-asserted-by":"publisher","unstructured":"Adams, M.: HOL zero\u2019s solutions for pollack-inconsistency. (eds Blanchette, J.\u00a0C. & Merz, S.) Interactive Theorem Proving (ITP), Vol. 9807 of Lecture Notes in Computer Science, 20\u201335 (Springer, 2016). https:\/\/doi.org\/10.1007\/978-3-319-43144-4_2","DOI":"10.1007\/978-3-319-43144-4_2"},{"key":"9743_CR15","doi-asserted-by":"publisher","unstructured":"Wiedijk, F.: Stateless HOL. (ed. Hirschowitz, T.) Types for Proofs and Programs (TYPES), Vol.\u00a053 of EPTCS, 47\u201361 (2009). https:\/\/doi.org\/10.4204\/EPTCS.53.4","DOI":"10.4204\/EPTCS.53.4"},{"key":"9743_CR16","doi-asserted-by":"publisher","unstructured":"Kanabar, H. et\u00a0al.:PureCake: A verified compiler for a lazy functional language. (ed. Foster, N.) Programming Language Design and Implementation (PLDI) (ACM, 2023). https:\/\/doi.org\/10.1145\/3591259","DOI":"10.1145\/3591259"},{"key":"9743_CR17","doi-asserted-by":"publisher","unstructured":"Harrison, J.: Towards self-verification of HOL Light. (eds Furbach, U. & Shankar, N.) Automated Reasoning (IJCAR), Vol. 4130 of LNCS (Springer, 2006). https:\/\/doi.org\/10.1007\/11814771_17","DOI":"10.1007\/11814771_17"},{"key":"9743_CR18","doi-asserted-by":"publisher","unstructured":"Pohjola, J.\u00a0\u00c5., Gengelbach, A.: A mechanised semantics for HOL with ad-hoc overloading. (eds Albert, E. & Kov\u00e1cs, L.) Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Vol.\u00a073 (EasyChair, 2020).https:\/\/doi.org\/10.29007\/413d","DOI":"10.29007\/413d"},{"key":"9743_CR19","doi-asserted-by":"publisher","unstructured":"Gengelbach, A., Pohjola, J.\u00a0\u00c5., Weber, T.: Mechanisation of model-theoretic conservative extension for HOL with ad-hoc overloading. (eds Coen, C.\u00a0S. & Tiu, A.) Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), Vol. 332 of EPTCS (2020). https:\/\/doi.org\/10.4204\/EPTCS.332.1","DOI":"10.4204\/EPTCS.332.1"},{"key":"9743_CR20","doi-asserted-by":"publisher","unstructured":"Gengelbach, A., Pohjola, J.\u00a0\u00c5.: A verified cyclicity checker: For theories with overloaded constants. (eds Andronick, J. & de\u00a0Moura, L.) Interactive Theorem Proving, ITP, Vol. 237 of LIPIcs, 15:1\u201315:18 (Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2022). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2022.15","DOI":"10.4230\/LIPIcs.ITP.2022.15"},{"key":"9743_CR21","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Ro\u00dfkopf, S.: Isabelle\u2019s metalogic: Formalization and proof checker. (eds Platzer, A. & Sutcliffe, G.) Automated Deduction (CADE), Vol. 12699 of LNCS (Springer, 2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_6","DOI":"10.1007\/978-3-030-79876-5_6"},{"key":"9743_CR22","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/s10817-015-9324-6","volume":"55","author":"J Davis","year":"2015","unstructured":"Davis, J., Myreen, M.O.: The reflective milawa theorem prover is sound (down to the machine code that runs it). J. Autom. Reason. 55, 117\u2013183 (2015). https:\/\/doi.org\/10.1007\/s10817-015-9324-6","journal-title":"J. Autom. Reason."},{"key":"9743_CR23","doi-asserted-by":"publisher","unstructured":"Carneiro, M.: Metamath Zero: Designing a theorem prover prover. (eds Benzm\u00fcller, C. & Miller, B.\u00a0R.) Intelligent Computer Mathematics (CICM), Vol. 12236 of LNCS (Springer, 2020). https:\/\/doi.org\/10.1007\/978-3-030-53518-6_5","DOI":"10.1007\/978-3-030-53518-6_5"},{"key":"9743_CR24","unstructured":"Carneiro, M.: Specifying verified x86 software from scratch. CoRRabs\/1907.01283 (2019). http:\/\/arxiv.org\/abs\/1907.01283"},{"key":"9743_CR25","doi-asserted-by":"publisher","unstructured":"Barras, B.: Sets in Coq, Coq in sets. J. Formaliz. Reason.3 (2010).https:\/\/doi.org\/10.6092\/issn.1972-5787\/1695","DOI":"10.6092\/issn.1972-5787\/1695"},{"key":"9743_CR26","doi-asserted-by":"publisher","unstructured":"Sozeau, M., Boulier, S., Forster, Y., Tabareau, N. & Winterhalter, T. Coq Coq correct! verification of type checking and erasure for Coq, in Coq. Proc. ACM Program. Lang.4 (2020). https:\/\/doi.org\/10.1145\/3371076","DOI":"10.1145\/3371076"},{"key":"9743_CR27","doi-asserted-by":"publisher","unstructured":"Anand, A., Rahli, V.: Towards a formally verified proof assistant. (eds Klein, G. & Gamboa, R.) Interactive Theorem Proving (ITP), Vol. 8558 of LNCS (Springer, 2014). https:\/\/doi.org\/10.1007\/978-3-319-08970-6_3","DOI":"10.1007\/978-3-319-08970-6_3"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09743-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-025-09743-8","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09743-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T08:50:26Z","timestamp":1766134226000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-025-09743-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,12]]},"references-count":27,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2025,12]]}},"alternative-id":["9743"],"URL":"https:\/\/doi.org\/10.1007\/s10817-025-09743-8","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2025,12]]},"assertion":[{"value":"22 April 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"30 September 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 December 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"32"}}