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.
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
We have developed and mechanically verified an ML system called CakeML, which supports a substantial subset of Standard ML. CakeML is implemented as an interactive read-eval-print loop (REPL) in x86-64 machine code. Our correctness theorem ensures that this REPL implementation prints only those results permitted by the semantics of CakeML. Our verification effort touches on a breadth of topics including lexing, parsing, type checking, incremental and dynamic compilation, garbage collection, arbitrary-precision arithmetic, and compiler bootstrapping.
How it got here
How it got here
agent via openalex
Added
2026-10-25 20:55 UTC
Not denied by
a person 2026-10-29 17:12 UTC
Cite it as
@misc{kumar2014cakeml,
title = {CakeML: A Verified Implementation of ML},
author = {Ramana Kumar and Magnus O. Myreen and Michael Norrish and Scott Owens},
year = {2014},
journal = {ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)},
pages = {179--191},
doi = {10.1145/2535838.2535841},
}