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; OpenTheory; OEuf; CAVA LTL Modelchecker; kepler98; OCaml; Flyspeck; Nitpick; ACL2
Cited in: 58 Publications
all top 5

Cited by 102 Authors

14 Myreen, Magnus O.
9 Kumar, Ramana
6 Norrish, Michael
5 Nipkow, Tobias
5 Owens, Scott
4 Tan, Yong Kiam
3 Abrahamsson, Oskar
3 Klein, Gerwin
3 Murray, Toby
3 Paulson, Lawrence Charles
3 Popescu, Andrei
3 Rizkallah, Christine
3 Sutcliffe, Geoff
2 Åman Pohjola, Johannes
2 Arthan, Rob D.
2 Bauereiß, Thomas
2 Chen, Zilin
2 Davis, Jared
2 Fox, Anthony C. J.
2 Heule, Marijn J. H.
2 Ho, Son Lam
2 Keller, Gabriele Cornelia
2 Lammich, Peter
2 Lim, Japheth
2 Lochbihler, Andreas
2 Nagashima, Yutaka
2 O’Connor, Liam
2 Pesenti Gritti, Armando
2 Rahli, Vincent
2 Raimondi, Franco
2 Roßkopf, Simon
2 Sandberg Ericsson, Adam
2 Sewell, Thomas D.
2 Wenzel, Makarius
1 Abel, Andreas M.
1 Allais, Guillaume
1 Amani, Sidney
1 Anand, Abhishek
1 Annenkov, Danil
1 Avigad, Jeremy
1 Ayala-Rincón, Mauricio
1 Baek, Seulkee
1 Bickford, Mark
1 Blanchette, Jasmin Christian
1 Brinkop, Hauke
1 Brown, Chad Edward
1 Chakravarty, Manuel M. T.
1 Cohen, Liron
1 Dam, Mads
1 Fava, Daniel Schnetzer
1 Garbuzov, Dmitri
1 Gauthier, Thibault
1 Gray, Kathryn E.
1 Guanciale, Roberto
1 Guéneau, Armaël
1 Hack, Sebastian
1 Hameer, Aliya
1 Hayes, Ian J.
1 Hou, Ping
1 Hupel, Lars
1 Immler, Fabian
1 Jantsch, Simon
1 Kaliszyk, Cezary
1 Kanabar, Hrutvik
1 Korovin, Konstantin
1 Krijnen, Jacco O. G.
1 Lindner, Andreas
1 López-Hernández, Julio César
1 Lundberg, Didrik
1 Mahboubi, Assia
1 Milo, Mikkel
1 Momigliano, Alberto
1 Mullen, Eric
1 Mulligan, Dominic P.
1 Muñoz, César A.
1 Nadathur, Gopalan
1 Nielsen, Jakob Botsch
1 Pattinson, Dirk
1 Pientka, Brigitte
1 Ridge, Thomas
1 Rosemann, Julian
1 Schäfer, Steven
1 Schneider, Sigurd
1 Sewell, Peter
1 Sibut-Pinote, Thomas
1 Sison, Robert
1 Snelting, Gregor
1 Spitters, Bas
1 Stark, Kathrin
1 Steffen, Martin
1 Stolz, Volker
1 Swierstra, Wouter
1 Tatlock, Zachary
1 Théry, Laurent
1 Tiwari, Mukesh
1 Tuerk, Thomas
1 Urban, Josef
1 Utting, Mark
1 Wang, Yuting
1 Webb, Brae J.
...and 2 more Authors

Citations by Year