Software:CakeML
From HandWiki
| Type | Compiler |
|---|---|
| Website | cakeml |
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
References
- ↑ CakeML: a verified implementation of ML. 2014. doi:10.1145/2578855.2535841. https://cakeml.org/popl14.pdf.
- ↑ Sandberg Ericsson, Adam; Myreen, Magnus O.; Åman Pohjola, Johannes (2019). "A Verified Generational Garbage Collector for CakeML". Journal of Automated Reasoning 63 (2): 463–488. doi:10.1007/s10817-018-9487-z. https://cakeml.org/itp17.pdf.
- ↑ 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. https://cacm.acm.org/magazines/2018/10/231372-formally-verified-software-in-the-real-world/fulltext.
External links
 |
