The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Verified compilation of CakeML to multiple machine-code targets
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
Abstract
This paper describes how the latest CakeML compiler supports verified compilation down to multiple realistically modelled target architectures. In particular, we describe how the compiler definition, the various language semantics, and the correctness proofs were organised to minimize target-specific overhead. With our setup we have incorporated compilation to four 64-bit architectures, ARMv8, x86-64, MIPS-64, RISC-V, and one 32-bit architecture, ARMv6. Our correctness theorem allows interference from the environment: the top-level correctness statement takes into account execution of foreign code and per-instruction interference from external processes, such as interrupt handlers in operating systems. The entire CakeML development is formalised in the HOL4 theorem prover.
How it got here
How it got here
agent via openalex
Added
2026-10-25 18:58 UTC
Not denied by
a person 2026-10-29 17:12 UTC
Cite it as
@misc{fox2016verified,
title = {Verified compilation of CakeML to multiple machine-code targets},
author = {Anthony C. J. Fox and Magnus O. Myreen and Yong Kiam Tan and Ramana Kumar},
year = {2016},
pages = {125--137},
doi = {10.1145/3018610.3018621},
}