About: Proof-Producing Synthesis of CakeML from Monadic HOL Functions

Not logged in : Login

(Sponging disallowed)

Facets (new session)
Description
Metadata
Settings
- Rule:
- Inverse Functional Properties:
- "Same As":

About: Proof-Producing Synthesis of CakeML from Monadic HOL Functions Goto Sponge NotDistinct Permalink

An Entity of Type : bibo:AcademicArticle, within Data Space : linkeddata.uriburner.com:28898 associated with source document(s)

Attributes	Values
type	http://eprints.org/ontology/ArticleEPrint http://eprints.org/ontology/EPrint Article Academic Article
seeAlso	HTML Summary of #82103 Proof-Producing Synthesis of CakeML from Monadic HOL Functions
sameAs	Proof-Producing Synthesis of CakeML from Monadic HOL Functions
http://eprints.org/ontology/hasDocument	Proof-Producing Synthesis of CakeML from Monadic HOL Functions (PDF) Proof-Producing Synthesis of CakeML from Monadic HOL Functions (Other) Proof-Producing Synthesis of CakeML from Monadic HOL Functions (Other) Proof-Producing Synthesis of CakeML from Monadic HOL Functions (Other) Proof-Producing Synthesis of CakeML from Monadic HOL Functions (Other) Proof-Producing Synthesis of CakeML from Monadic HOL Functions (Other)
http://eprints.org/ontology/hasPublished	Proof-Producing Synthesis of CakeML from Monadic HOL Functions (PDF)
dc:hasVersion	Proof-Producing Synthesis of CakeML from Monadic HOL Functions (PDF)
Title	Proof-Producing Synthesis of CakeML from Monadic HOL Functions
described by	https://demo.openlinksw.com/about/id/entity/https/www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/export_kar_RDFN3.n3 https://demo.openlinksw.com/about/id/entity/https/raw.githubusercontent.com/annajordanous/CO644Files/main/export_kar_RDFN3.n3
Date	2020-06-06
Creator	Oskar Abrahamsson Michael Norrish Son Ho Yong Kiam Tan Ramana Kumar Magnus O. Myreen Hrutvik Kanabar
status	peer reviewed published
Publisher	Springer
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 instruction encoder 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.
Is Part Of	Journal of Automated Reasoning https://kar.kent.ac.uk/id/repository
Subject	Q Science QA 76 Software, computer programming,
list of authors	https://kar.kent.ac.uk/id/eprint/82103#authors
is topic of	https://www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/export_kar_RDFN3.n3 https://raw.githubusercontent.com/annajordanous/CO644Files/main/export_kar_RDFN3.n3
is primary topic of	HTML Summary of #82103 Proof-Producing Synthesis of CakeML from Monadic HOL Functions

Faceted Search & Find service v1.17_git144 as of Jul 26 2024

Alternative Linked Data Documents: iSPARQL | ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 08.03.3331 as of Aug 25 2024, on Linux (x86_64-ubuntu_noble-linux-glibc2.38-64), Single-Server Edition (378 GB total memory, 62 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software