{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T10:11:28Z","timestamp":1766139088774,"version":"3.40.2"},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2025,2,18]],"date-time":"2025-02-18T00:00:00Z","timestamp":1739836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,2,18]],"date-time":"2025-02-18T00:00:00Z","timestamp":1739836800000},"content-version":"vor","delay-in-days":0,"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,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>We add an efficient function for computation to the kernels of higher-order logic interactive theorem provers. First, we develop and prove sound our approach for Candle. Candle is a port of HOL Light which has been proved sound with respect to the inference rules of its higher-order logic; we extend its implementation and soundness proof. Second, we replicate our now-verified implementation for HOL4 with only minor changes, and build additional automation for ease of use. The automation exists outside of the HOL4 kernel, and requires no additional trust. We exercise our new computation function and associated automation on the evaluation of the CakeML compiler backend within HOL4\u2019s logic, demonstrating an order of magnitude speedup. This is an extended version of our previous conference paper [2], which described implementation and soundness proofs for Candle. Our HOL4 implementation and automation are new, as are the CakeML benchmarks.<\/jats:p>","DOI":"10.1007\/s10817-025-09719-8","type":"journal-article","created":{"date-parts":[[2025,2,18]],"date-time":"2025-02-18T11:40:52Z","timestamp":1739878852000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Fast, Verified Computation for HOL ITPs"],"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":"Michael","family":"Norrish","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hrutvik","family":"Kanabar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Johannes \u00c5man","family":"Pohjola","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,2,18]]},"reference":[{"key":"9719_CR1","unstructured":"Abrahamsson, O., Myreen, M.O., Kumar, R., Sewell, T.: Candle: a verified implementation of HOL Light. In: Andronick, J., de\u00a0Moura, L. (eds.) Interactive Theorem Proving (ITP). LIPIcs, vol. 237, pp. 3:1\u20133:17 Springer, Cham (2022)"},{"key":"9719_CR2","doi-asserted-by":"publisher","unstructured":"Abrahamsson, O., Myreen, M.O.: Fast, verified computation for Candle. In: Naumowicz, A., Thiemann, R. (eds.) Interactive Theorem Proving (ITP). LIPIcs, vol. 268, pp. 4:1\u20134:17. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2023.4","DOI":"10.4230\/LIPIcs.ITP.2023.4"},{"key":"9719_CR3","unstructured":"Abrahamsson, O.: A verified theorem prover for higher-order logic. PhD thesis, Chalmers University of Technology (2022)"},{"key":"9719_CR4","doi-asserted-by":"publisher","first-page":"1287","DOI":"10.1007\/s10817-020-09559-8","volume":"64","author":"O Abrahamsson","year":"2020","unstructured":"Abrahamsson, O., et al.: Proof-producing synthesis of CakeML from monadic HOL functions. J. Autom. Reason. 64, 1287\u20131306 (2020)","journal-title":"J. Autom. Reason."},{"key":"9719_CR5","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1017\/S0956796812000019","volume":"22","author":"K Aehlig","year":"2012","unstructured":"Aehlig, K., Haftmann, F., Nipkow, T.: A compiled implementation of normalisation by evaluation. J. Funct. Program. 22, 9\u201330 (2012)","journal-title":"J. Funct. Program."},{"key":"9719_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/3-540-44659-1_2","volume-title":"Theorem Proving in Higher Order Logics (TPHOLs)","author":"B Barras","year":"2000","unstructured":"Barras, B.: Programming and computing in HOL. In: Aagaard, M., Harrison, J. (eds.) Theorem Proving in Higher Order Logics (TPHOLs). Lecture Notes in Computer Science, vol. 1869, pp. 17\u201337. Springer, Berlin (2000)"},{"key":"9719_CR7","first-page":"333","volume-title":"Conference on LISP and Functional Programming (LFP)","author":"P Cr\u00e9gut","year":"1990","unstructured":"Cr\u00e9gut, P.: An abstract machine for lambda-terms normalization. In: Kahn, G. (ed.) Conference on LISP and Functional Programming (LFP), pp. 333\u2013340. ACM, New York (1990)"},{"key":"9719_CR8","doi-asserted-by":"crossref","unstructured":"Danvy, O., Nielsen, L.R.: Defunctionalization at work. Tech. Rep. BRICS RS-01-23, BRICS, Department of Computer Science, University of Aarhus (2001)","DOI":"10.7146\/brics.v8i23.21684"},{"key":"9719_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"625","DOI":"10.1007\/978-3-030-79876-5_37","volume-title":"International Conference on Automated Deduction (CADE)","author":"L de Moura","year":"2021","unstructured":"de Moura, L., Ullrich, S.: The Lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) International Conference on Automated Deduction (CADE). Lecture Notes in Computer Science, vol. 12699, pp. 625\u2013635. Springer, Berlin (2021)"},{"key":"9719_CR10","first-page":"235","volume-title":"International Conference on Functional Programming (ICFP)","author":"B Gr\u00e9goire","year":"2002","unstructured":"Gr\u00e9goire, B., Leroy, X.: A compiled implementation of strong reduction. In: Wand, M., Jones, S.L.P. (eds.) International Conference on Functional Programming (ICFP), pp. 235\u2013246. ACM, New York (2002)"},{"key":"9719_CR11","unstructured":"Haftmann, F.: Code generation from specifications in higher-order logic. PhD thesis, Technical University Munich (2009)"},{"key":"9719_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-12251-4_9","volume-title":"Functional and Logic Programming (FLOPS)","author":"F Haftmann","year":"2010","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) Functional and Logic Programming (FLOPS). Lecture Notes in Computer Science, vol. 6009, pp. 103\u2013117. Springer, Berlin (2010)"},{"key":"9719_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-03359-9_4","volume-title":"Theorem Proving in Higher Order Logics (TPHOLs)","author":"J Harrison","year":"2009","unstructured":"Harrison, J.: HOL light: an overview. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) Theorem Proving in Higher Order Logics (TPHOLs). Lecture Notes in Computer Science, vol. 5674, pp. 60\u201366. Springer, Berlin (2009)"},{"key":"9719_CR14","doi-asserted-by":"publisher","unstructured":"Kumar, R., Norrish, M.: (nominal) unification by recursive descent with triangular substitutions. In: Kaufmann, M., Paulson, L.C. (eds.) Interactive Theorem Proving\u00a0(ITP), 2010. Proceedings. Lecture Notes in Computer Science, vol. 6172, pp. 51\u201366. Springer, Berlin (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_6","DOI":"10.1007\/978-3-642-14052-5_6"},{"key":"9719_CR15","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1145\/2535838.2535841","volume-title":"Principles of Programming Languages (POPL)","author":"R Kumar","year":"2014","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Jagannathan, S., Sewell, P. (eds.) Principles of Programming Languages (POPL), pp. 179\u2013192. ACM, New York (2014). https:\/\/doi.org\/10.1145\/2535838.2535841"},{"key":"9719_CR16","doi-asserted-by":"publisher","first-page":"1041","DOI":"10.1145\/3314221.3314622","volume-title":"Programming Language Design and Implementation (PLDI)","author":"A L\u00f6\u00f6w","year":"2019","unstructured":"L\u00f6\u00f6w, A., et al.: Verified compilation on a verified processor. In: McKinley, K.S., Fisher, K. (eds.) Programming Language Design and Implementation (PLDI), pp. 1041\u20131053. ACM, New York (2019). https:\/\/doi.org\/10.1145\/3314221.3314622"},{"key":"9719_CR17","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1145\/3437992.3439915","volume-title":"International Conference on Certified Programs and Proofs (CPP)","author":"MO Myreen","year":"2021","unstructured":"Myreen, M.O.: A minimalistic verified bootstrapped compiler (proof pearl). In: Hritcu, C., Popescu, A. (eds.) International Conference on Certified Programs and Proofs (CPP), pp. 32\u201345. ACM, New York (2021). https:\/\/doi.org\/10.1145\/3437992.3439915"},{"key":"9719_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283. Springer, Berlin (2002)"},{"key":"9719_CR19","doi-asserted-by":"publisher","unstructured":"Pohjola, J.\u00a0\u00c5., Rostedt, H., Myreen, M.O.: Characteristic formulae for liveness properties of non-terminating CakeML programs. In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) Interactive Theorem Proving, ITP. LIPIcs, vol. 141, pp. 32:1\u201332:19. Schloss Dagstuhl-Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.32","DOI":"10.4230\/LIPIcs.ITP.2019.32"},{"key":"9719_CR20","doi-asserted-by":"crossref","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) Theorem Proving in Higher Order Logics (TPHOLs). LNCS, vol. 5170. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-71067-7_6"},{"key":"9719_CR21","unstructured":"Solovyev, A.: HOL Light\u2019s computelib. https:\/\/github.com\/jrh13\/hol-light\/blob\/master\/compute.ml. Accessed 11 June 2022"},{"key":"9719_CR22","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000229","author":"YK Tan","year":"2019","unstructured":"Tan, Y.K., et al.: The verified CakeML compiler backend. J. Funct. Program. (2019). https:\/\/doi.org\/10.1017\/S0956796818000229","journal-title":"J. Funct. Program."},{"key":"9719_CR23","volume-title":"Implementation and Application of Functional Programming Languages (IFL)","author":"YK Tan","year":"2015","unstructured":"Tan, Y.K., Owens, S., Kumar, R.: A verified type system for CakeML. In: L\u00e4mmel, R. (ed.) Implementation and Application of Functional Programming Languages (IFL). ACM, New York (2015)"},{"key":"9719_CR24","unstructured":"The Coq Development Team: The Coq reference manual. https:\/\/coq.inria.fr\/distrib\/current\/refman\/. Accessed 11 June 2022"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09719-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-025-09719-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09719-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T20:52:35Z","timestamp":1742676755000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-025-09719-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,2,18]]},"references-count":24,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,3]]}},"alternative-id":["9719"],"URL":"https:\/\/doi.org\/10.1007\/s10817-025-09719-8","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2025,2,18]]},"assertion":[{"value":"29 April 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 January 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 February 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"7"}}