Cultural advice

The Australian National University acknowledges, celebrates and pays our respects to the Ngunnawal and Ngambri people of the Canberra region and to all First Nations Australians on whose traditional lands we meet and work, and whose cultures are among the oldest continuing cultures in human history.

Aboriginal and Torres Strait Islander peoples are advised that ANU Library collections may include images, names, voices, and other representations of deceased persons.

Material in the collection may contain terms, language or views that reflect the period in which the item was created and may be considered inappropriate today.

Fast, Verified Computation for HOL ITPs

Simple item page
dc.contributor.authorAbrahamsson, Oskaren
dc.contributor.authorMyreen, Magnus O.en
dc.contributor.authorNorrish, Michaelen
dc.contributor.authorKanabar, Hrutviken
dc.contributor.authorPohjola, Johannes Åmanen
dc.date.accessioned2025-05-23T14:20:50Z
dc.date.available2025-05-23T14:20:50Z
dc.date.issued2025en
dc.description.abstractWe 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’s 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.en
dc.description.sponsorshipOpen access funding provided by University of Gothenburg. We want to thank Jeremy Avigad, John Harrison, Tobias Nipkow and Freek Wiedijk for feedback we received when the first author prepared this as a chapter for his PhD thesis []. We thank Thomas Sewell for showing us how to benchmark in-logic evaluation in Isabelle/HOL; and Paulo Torrens for pointing at us some relevant literature for CPS translation and defunctionalisation. The first two authors were supported by the Swedish Foundation for Strategic Research.en
dc.description.statusPeer-revieweden
dc.format.extent40en
dc.identifier.issn0168-7433en
dc.identifier.otherORCID:/0000-0003-1163-8467/work/184101075en
dc.identifier.scopus85218426977en
dc.identifier.urihttp://www.scopus.com/inward/record.url?scp=85218426977&partnerID=8YFLogxKen
dc.identifier.urihttps://hdl.handle.net/1885/733752408
dc.language.isoenen
dc.provenanceThis article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.en
dc.rights ©2025 The Author(s) en
dc.sourceJournal of Automated Reasoningen
dc.subjectHigher-order logicen
dc.subjectInteractive theorem provingen
dc.subjectProver soundnessen
dc.titleFast, Verified Computation for HOL ITPsen
dc.typeJournal articleen
dspace.entity.typePublicationen
local.contributor.affiliationAbrahamsson, Oskar; Chalmers University of Technologyen
local.contributor.affiliationMyreen, Magnus O.; Chalmers University of Technologyen
local.contributor.affiliationNorrish, Michael; Mathematical Sciences Institute Administration, Mathematical Sciences Institute, ANU College of Systems and Society, The Australian National Universityen
local.contributor.affiliationKanabar, Hrutvik; ARM Ltd.en
local.contributor.affiliationPohjola, Johannes Åman; Chalmers University of Technologyen
local.identifier.citationvolume69en
local.identifier.doi10.1007/s10817-025-09719-8en
local.identifier.pure7c4a2937-250d-44ef-afbe-a54bcd536c15en
local.identifier.urlhttps://www.scopus.com/pages/publications/85218426977en
local.type.statusPublisheden

Downloads

Original bundle

Now showing 1 - 1 of 1
Thumbnail Image
Name:
s10817-025-09719-8.pdf
Size:
841.68 KB
Format:
Adobe Portable Document Format
Download

Collections

ANU Research Publications

DSpace software copyright © 2002-2026 LYRASIS

abcd