Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions

dc.contributor.authorHo, Son
dc.contributor.authorAbrahamsson, Oskar
dc.contributor.authorKumar, Ramana
dc.contributor.authorMyreen, Magnus
dc.contributor.authorTan, Yong Kiam
dc.contributor.authorNorrish, Michael
dc.contributor.editorSebastiani, R
dc.contributor.editorGalmiche, D
dc.contributor.editorSchulz, S
dc.coverage.spatialOxford, United Kingdom
dc.date.accessioned2024-02-12T22:44:39Z
dc.date.createdJuly 14-17 2018
dc.date.issued2018
dc.date.updated2022-10-02T07:19:30Z
dc.description.abstractWe introduce an automatic method for producing stateful ML programs together with proofs of correctness from monadic functions in HOL. Our mechanism supports references, exceptions, and I/O operations, and can generate functions manipulating local state, which can then be encapsulated for use in a pure context. We apply this approach to several non-trivial examples, including the type inferencer and register allocator of the otherwise pure CakeML compiler, which now benefits from better runtime performance. This development has been carried out in the HOL4 theorem prover.en_AU
dc.description.sponsorshipThe second and fourth authors were partly supported by the Swedish Foundation for Strategic Research.en_AU
dc.format.mimetypeapplication/pdfen_AU
dc.identifier.isbn978-331994204-9en_AU
dc.identifier.urihttp://hdl.handle.net/1885/313420
dc.language.isoen_AUen_AU
dc.publisherSpringer Verlagen_AU
dc.relation.ispartofseries9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018en_AU
dc.rights© Springer International Publishing AG, part of Springer Nature 2018en_AU
dc.sourceLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)en_AU
dc.titleProof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functionsen_AU
dc.typeConference paperen_AU
local.bibliographicCitation.lastpage662en_AU
local.bibliographicCitation.startpage646en_AU
local.contributor.affiliationHo, Son, PSL Research Universityen_AU
local.contributor.affiliationAbrahamsson, Oskar, Chalmers University of Technologyen_AU
local.contributor.affiliationKumar, Ramana, CSIRO/UNSWen_AU
local.contributor.affiliationMyreen, Magnus, Chalmers University of Technologyen_AU
local.contributor.affiliationTan, Yong Kiam, Carnegie Mellon Universityen_AU
local.contributor.affiliationNorrish, Michael, College of Engineering and Computer Science, ANUen_AU
local.contributor.authoremailu4087502@anu.edu.auen_AU
local.contributor.authoruidNorrish, Michael, u4087502en_AU
local.description.embargo2099-12-31
local.description.notesImported from ARIESen_AU
local.description.refereedYes
local.identifier.absfor461204 - Programming languagesen_AU
local.identifier.absfor461203 - Formal methods for softwareen_AU
local.identifier.absfor461303 - Computational logic and formal languagesen_AU
local.identifier.ariespublicationu3102795xPUB1757en_AU
local.identifier.doi10.1007/978-3-319-94205-6_42en_AU
local.identifier.scopusID2-s2.0-85049930435
local.identifier.thomsonIDWOS:000470004600041
local.identifier.uidSubmittedByu3102795en_AU
local.publisher.urlhttps://link.springer.com/en_AU
local.type.statusPublished Versionen_AU

Downloads

Original bundle

Now showing 1 - 1 of 1
No Thumbnail Available
Name:
978-3-319-94205-6_42.pdf
Size:
329.8 KB
Format:
Adobe Portable Document Format
Description:
Back to topicon-arrow-up-solid
 
APRU
IARU
 
edX
Group of Eight Member

Acknowledgement of Country

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.


Contact ANUCopyrightDisclaimerPrivacyFreedom of Information

+61 2 6125 5111 The Australian National University, Canberra

TEQSA Provider ID: PRV12002 (Australian University) CRICOS Provider Code: 00120C ABN: 52 234 063 906