## CakeML

swMATH ID: | 8799 |

Software Authors: | Kumar, Ramana; Myreen, Magnus O.; Norrish, Michael; Owens, Scott |

Description: | Cakeml, a verified implementation of ML. 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.Our contributions are twofold. The first is simply in building a system that is end-to-end verified, demonstrating that each piece of such a verification effort can in practice be composed with the others, and ensuring that none of the pieces rely on any over-simplifying assumptions. The second is developing novel approaches to some of the more challenging aspects of the verification. In particular, our formally verified compiler can bootstrap itself: we apply the verified compiler to itself to produce a verified machine-code implementation of the compiler. Additionally, our compiler proof handles diverging input programs with a lightweight approach based on logical timeout exceptions. The entire development was carried out in the HOL4 theorem prover. |

Homepage: | https://cakeml.org/ |

Keywords: | ML; compiler bootstrapping; compiler verification; machine code verification; read-eval-print loop; verified garbage collection; verified parsing; verified type checking |

Related Software: | Isabelle/HOL; Coq; HOL; HOL Light; seL4; Isabelle; CertiCoq; Archive Formal Proofs; Sledgehammer; Milawa; Jitawa; CompCert; OEuf; CAVA LTL Modelchecker; kepler98; OCaml; Flyspeck; Nitpick; ACL2; GitHub |

Cited in: | 57 Publications |

all
top 5

### Cited by 102 Authors

all
top 5

### Cited in 10 Serials

all
top 5