CakeML
| Engine | |
|---|---|
| Type | Compiler |
| Website | cakeml |
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]
- ↑ "CakeML: a verified implementation of ML" (PDF). 2014. doi:10.1145/2578855.2535841.
- ↑ 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) - ↑ 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 software article is a stub. You can help EverybodyWiki by expanding it. |
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.
