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; Isabelle; Archive Formal Proofs; seL4; CertiCoq; Milawa; Jitawa; Sledgehammer; CompCert; CAVA LTL Modelchecker; OpenTheory; OEuf; DRAT-trim; GitHub; LCF; Agda; kepler98
Cited in: 67 Documents
all top 5

Cited by 121 Authors

16 Myreen, Magnus O.
9 Kumar, Ramana
6 Norrish, Michael
5 Nipkow, Tobias
5 Owens, Scott
4 Abrahamsson, Oskar
4 Popescu, Andrei
4 Rizkallah, Christine
4 Tan, Yong Kiam
3 Heule, Marijn J. H.
3 Klein, Gerwin
3 Lammich, Peter
3 Murray, Toby
3 Paulson, Lawrence Charles
3 Sutcliffe, Geoff
3 Wenzel, Makarius
2 Åman Pohjola, Johannes
2 Arthan, Rob D.
2 Bauereiß, Thomas
2 Chen, Zilin
2 Davis, Jared
2 Fox, Anthony C. J.
2 Ho, Son Lam
2 Immler, Fabian
2 Keller, Gabriele Cornelia
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.
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 Breitner, Joachim
1 Brinkop, Hauke
1 Brown, Chad Edward
1 Bryant, Randal E.
1 Chakravarty, Manuel M. T.
1 Chlipala, Adam J.
1 Cohen, Joshua M.
1 Cohen, Liron
1 Cordwell, Katherine
1 Dam, Mads
1 Delaware, Benjamin
1 Fava, Daniel Schnetzer
1 Forster, Yannick
1 Garbuzov, Dmitri
1 Gauthier, Thibault
1 Gray, Kathryn E.
1 Gross, Jason
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 Jantsch, Simon
1 Kaliszyk, Cezary
1 Kanabar, Hrutvik
1 Korovin, Konstantin
1 Krijnen, Jacco O. G.
1 Kunze, Fabian
1 Li, Yao
1 Lindner, Andreas
1 López-Hernández, Julio César
1 Lundberg, Didrik
1 Mahboubi, Assia
1 Milo, Mikkel
1 Mitsch, Stefan
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 Pit-Claudel, Clément
1 Platzer, André
1 Rädle, Jonas
1 Ridge, Thomas
1 Rosemann, Julian
1 Schäfer, Steven
1 Scharager, Matias
1 Schneider, Sigurd
1 Sewell, Peter
1 Sibut-Pinote, Thomas
...and 21 more Authors

Citations by Year