@inproceedings{kumar_cakeml_2014,
 title = {{CakeML}: a verified implementation of {ML}},
 author = {Kumar, Ramana and Myreen, Magnus O. and Norrish, Michael and Owens, Scott},
 year = {2014},
 isbn = {978-1-4503-2544-8},
 doi = {10.1145/2535838.2535841},
 url = {https://dl.acm.org/doi/10.1145/2535838.2535841},
 urldate = {2024-04-22},
 booktitle = {Proceedings of the 41st {ACM} {SIGPLAN}-{SIGACT} {Symposium} on {Principles} of {Programming} {Languages}},
 pages = {179--191},
 publisher = {ACM},
 address = {San Diego California USA},
 month = {January},
 language = {en},
 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, arbitraryprecision arithmetic, and compiler bootstrapping.},
 shorttitle = {{CakeML}}
}