You can edit almost every page by Creating an account. Otherwise, see the FAQ.

CakeML

From EverybodyWiki Bios & Wiki







CakeML
Engine
    TypeCompiler
    Websitecakeml.org

    Search CakeML on Amazon.

    CakeML is a formally verified optimizing compiler for a substantial subset of Standard ML.[1] It can target ARM, AArch64, x86-64, MIPS (64-bit), and RISC-V (64-bit). The specification, implementation, and proof is written in HOL4.

    CakeML includes the first formally verified generational garbage collector.[2]

    In October 2018 issue of Communications of the ACM,[3] CakeML got named among "a number of impressive breakthroughs", together with CompCert and seL4.

    See also[edit]

    References[edit]

    1. "CakeML: a verified implementation of ML" (PDF). 2014. doi:10.1145/2578855.2535841.
    2. Sandberg Ericsson, Adam; Myreen, Magnus O.; Åman Pohjola, Johannes (2019). "A Verified Generational Garbage Collector for CakeML" (PDF). Journal of Automated Reasoning. 63 (2): 463–488. doi:10.1007/s10817-018-9487-z. Unknown parameter |s2cid= ignored (help)
    3. Klein, Gerwin; Andronick, June; Fernandez, Matthew; Kuz, Ihor; Murray, Toby; Heiser, Gernot (2018). "Formally Verified Software in the Real World". Communications of the ACM. 61 (10): 68–77. doi:10.1145/3230627. Unknown parameter |s2cid= ignored (help)

    External links[edit]



    This article "CakeML" is from Wikipedia. The list of its authors can be seen in its historical and/or the page Edithistory:CakeML. Articles copied from Draft Namespace on Wikipedia could be seen on the Draft Namespace of Wikipedia and not main one.