Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions
dc.contributor.author | Ho, Son | |
dc.contributor.author | Abrahamsson, Oskar | |
dc.contributor.author | Kumar, Ramana | |
dc.contributor.author | Myreen, Magnus | |
dc.contributor.author | Tan, Yong Kiam | |
dc.contributor.author | Norrish, Michael | |
dc.contributor.editor | Sebastiani, R | |
dc.contributor.editor | Galmiche, D | |
dc.contributor.editor | Schulz, S | |
dc.coverage.spatial | Oxford, United Kingdom | |
dc.date.accessioned | 2024-02-12T22:44:39Z | |
dc.date.created | July 14-17 2018 | |
dc.date.issued | 2018 | |
dc.date.updated | 2022-10-02T07:19:30Z | |
dc.description.abstract | We 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.sponsorship | The second and fourth authors were partly supported by the Swedish Foundation for Strategic Research. | en_AU |
dc.format.mimetype | application/pdf | en_AU |
dc.identifier.isbn | 978-331994204-9 | en_AU |
dc.identifier.uri | http://hdl.handle.net/1885/313420 | |
dc.language.iso | en_AU | en_AU |
dc.publisher | Springer Verlag | en_AU |
dc.relation.ispartofseries | 9th International Joint Conference on Automated Reasoning, IJCAR 2018 Held as Part of the Federated Logic Conference, FloC 2018 | en_AU |
dc.rights | © Springer International Publishing AG, part of Springer Nature 2018 | en_AU |
dc.source | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) | en_AU |
dc.title | Proof-Producing Synthesis of CakeML with I/O and Local State from Monadic HOL Functions | en_AU |
dc.type | Conference paper | en_AU |
local.bibliographicCitation.lastpage | 662 | en_AU |
local.bibliographicCitation.startpage | 646 | en_AU |
local.contributor.affiliation | Ho, Son, PSL Research University | en_AU |
local.contributor.affiliation | Abrahamsson, Oskar, Chalmers University of Technology | en_AU |
local.contributor.affiliation | Kumar, Ramana, CSIRO/UNSW | en_AU |
local.contributor.affiliation | Myreen, Magnus, Chalmers University of Technology | en_AU |
local.contributor.affiliation | Tan, Yong Kiam, Carnegie Mellon University | en_AU |
local.contributor.affiliation | Norrish, Michael, College of Engineering and Computer Science, ANU | en_AU |
local.contributor.authoremail | u4087502@anu.edu.au | en_AU |
local.contributor.authoruid | Norrish, Michael, u4087502 | en_AU |
local.description.embargo | 2099-12-31 | |
local.description.notes | Imported from ARIES | en_AU |
local.description.refereed | Yes | |
local.identifier.absfor | 461204 - Programming languages | en_AU |
local.identifier.absfor | 461203 - Formal methods for software | en_AU |
local.identifier.absfor | 461303 - Computational logic and formal languages | en_AU |
local.identifier.ariespublication | u3102795xPUB1757 | en_AU |
local.identifier.doi | 10.1007/978-3-319-94205-6_42 | en_AU |
local.identifier.scopusID | 2-s2.0-85049930435 | |
local.identifier.thomsonID | WOS:000470004600041 | |
local.identifier.uidSubmittedBy | u3102795 | en_AU |
local.publisher.url | https://link.springer.com/ | en_AU |
local.type.status | Published Version | en_AU |
Downloads
Original bundle
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: