About: The Verified CakeML Compiler Backend

Not logged in : Login

(Sponging disallowed)

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

About: The Verified CakeML Compiler Backend 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 #71304 The Verified CakeML Compiler Backend
sameAs	The Verified CakeML Compiler Backend
http://eprints.org/ontology/hasAccepted	The Verified CakeML Compiler Backend (PDF)
http://eprints.org/ontology/hasDocument	The Verified CakeML Compiler Backend (PDF) The Verified CakeML Compiler Backend (Other) The Verified CakeML Compiler Backend (Other) The Verified CakeML Compiler Backend (Other) The Verified CakeML Compiler Backend (Other) The Verified CakeML Compiler Backend (Other)
dc:hasVersion	The Verified CakeML Compiler Backend (PDF)
Title	The Verified CakeML Compiler Backend
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	2019-02-04
Creator	Anthony Fox Ramana Kumar Magnus O. Myreen Michael Norrish Yong Kiam Tan Scott Owens
status	peer reviewed published
Publisher	Cambridge University Press
abstract	The CakeML compiler is, to the best of our knowledge, the most realistic veri?ed compiler for a functional programming language to date. The architecture of the compiler, a sequence of intermediate languages through which high-level features are compiled away incrementally, enables veri?cation of each compilation pass at inappropriate level of semantic detail.Partsofthecompiler’s implementation resemble mainstream (unveri?ed) compilers for strict functional languages, and it support several important features and optimisations. These include ef?cient curried multi-argument functions, con?gurable data representations, ef?cient exceptions, register allocation,and more. The compiler produces machine code for ?ve architectures: x86-64, ARMv6, ARMv8, MIPS-64, and RISC-V. The generatedmachine code contains the veri?edruntime system which includes averi?ed generational copying garbage collect or and averi?edarbitraryprecisionarithmetic(bignum)library. In this paper we present the overall design of the compiler backend, including its 12 intermediate languages. We explain how the semantics and proofs ?t together, and provide detail on how the compiler has been bootstrapped inside the logic of a theorem prover. The entire development has been carried out within the HOL4 theorem prover.
Is Part Of	Journal of Functional Programming https://kar.kent.ac.uk/id/repository
Subject	QA 76 Software, computer programming,
list of authors	https://kar.kent.ac.uk/id/eprint/71304#authors
volume	29
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 #71304 The Verified CakeML Compiler Backend

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, 36 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software