CakeML
CakeML is a functional programming language with a proven-correct compiler.
Aim
Reducing the cost and increasing the guarantees of verified software.
Approach
- Verified compilation: we have developed the world-leading verified optimising compiler (and runtime system) for functional programming.
- Proof-producing code generation: we have developed methods for automatically producing (verified) CakeML implementations of algorithms defined and verified in higher-order logic.
Further information
See the CakeML project website.
People
Publications
These are publications involving Trustworthy Systems researchers. See the CakeML publications list for other publications.
|
 |
Johannes Åman Pohjola, Hira Taqdees Syeda, Miki Tanaka, Krishnan Winter, Gordon Sau, Ben Nott, Tiana Tsang Ung, Craig McLaughlin, Remy Seassau, Magnus Myreen, Michael Norrish and Gernot Heiser Pancake: verified systems programming made sweeter Workshop on Programming Languages and Operating Systems (PLOS), Koblenz, DE, October, 2023 |
|
|
Hrutvik Kanabar, Samuel Vivien, Oskar Abrahamsson, Magnus Myreen, Michael Norrish, Johannes Åman Pohjola and Riccardo Zanetti Purecake: A verified compiler for a lazy functional language Proc. ACM Program. Lang., Volume 7, Number PLDI, pp. 952–976, 2023 |
|
|
|
Arve Gengelbach and Johannes Åman Pohjola A verified cyclicity checker: For theories with overloaded constants International Conference on Interactive Theorem Proving, pp. 15:1–15:18, Haifa, Israel, August, 2022 |
|
|
|
Johannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker and Michael Norrish Kalas: A verified, end-to-end compiler for a choreographic language International Conference on Interactive Theorem Proving, pp. 27:1–27:18, Haifa, Israel, August, 2022 |
|
|
 |
Alejandro Gomez-Londono, Johannes Åman Pohjola, Hira Taqdees Syeda, Magnus Myreen and Yong Kiam Tan Do you have space for dessert? A verified space cost semantics for CakeML programs OOPSLA, pp. 204:1-29, Chicago, IL, November, 2020 |
|
|
|
Johannes Åman Pohjola and Arve Gengelbach A mechanised semantics for HOL with ad-hoc overloading LPAR23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 498-515, Alicante, Spain, May, 2020 |
|
|
|
Gernot Heiser, Gerwin Klein and June Andronick seL4 in Australia: From research to real-world trustworthy systems Communications of the ACM, Volume 63, Issue 4, pp. 72-75, April, 2020 |
|
|
|
Konrad Slind, David Hardin, Johannes Åman Pohjola and Michael Sproul Synthesis of verified architectural components for autonomy hosted on a verified microkernel Hawaii International Conference on System Sciences, pp. 6365-6374, Grand Wilea, Hawaii, January, 2020 |
|
|
|
Johannes Åman Pohjola, Henrik Rostedt and Magnus Myreen Characteristic formulae for liveness properties of non-terminating CakeML programs International Conference on Interactive Theorem Proving, pp. 32:1-19, Portland, Oregon, September, 2019 |
|
|
|
Adam Sandberg Ericsson, Magnus Myreen and Johannes Åman Pohjola A verified generational garbage collector for CakeML Journal of Automated Reasoning, Volume 63, Issue 2, pp. 463–488, August, 2019 |
|
|
|
Andreas Lööw, Ramana Kumar, Yong Kiam Tan, Magnus Myreen, Michael Norrish, Oskar Abrahamsson and Anthony Fox Verified compilation on a verified processor ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 1041-1053, Phoenix, Arizona, United States of America, June, 2019 |
|
|
|
Yong Kiam Tan, Magnus Myreen, Ramana Kumar, Anthony Fox, Scott Owens and Michael Norrish The verified CakeML compiler backend Journal of Functional Programming, Volume 29, February, 2019 |
|
|
|
Milad Ghale, Dirk Pattinson, Ramana Kumar and Michael Norrish Verified certificate checking for counting votes Verified Software: Theories, Tools and Experiments, pp. 69–87, Oxford, December, 2018 |
|
|
|
Hugo Feree, Johannes Åman Pohjola, Ramana Kumar, Scott Owens, Magnus Myreen and Son Ho Program verification in the presence of I/O: semantics, verified library routines, and verified applications Verified Software: Theories, Tools and Experiments, pp. 88-111, Oxford, UK, November, 2018 |
|
|
|
Alejandro Gomez-Londono and Johannes Åman Pohjola Connecting choreography languages with verified stacks at Nordic Workshop on Programming Theory, Oslo, Norway, October, 2018 |
|
|
|
Son Ho, Oskar Abrahamsson, Ramana Kumar, Magnus Myreen, Yong Kiam Tan and Michael Norrish Proof-producing synthesis of CakeML with I/O and local state from monadic HOL functions International Joint Conference on Automated Reasoning, pp. 646-662, Oxford, July, 2018 |
|
|
|
Simon Jantsch and Michael Norrish Verifying the LTL to Büchi automata translation via very weak alternating automata International Conference on Interactive Theorem Proving, pp. 306-323, Oxford, July, 2018 |
|
|
|
Scott Owens, Michael Norrish, Ramana Kumar, Yong Kiam Tan and Magnus Myreen Verifying efficient function calls in CakeML International Conference on Functional Programming, Oxford, September, 2017 |
|
|
|
Armaël Guéneau, Magnus Myreen, Ramana Kumar and Michael Norrish Verified characteristic formulae for CakeML European Symposium on Programming, pp. 584–610, Uppsala, Sweden, April, 2017 |
|
|
|
Armaël Guéneau, Magnus Myreen, Ramana Kumar and Michael Norrish Verified characteristic formulae for CakeML European Symposium on Programming, pp. 584-610, Uppsala, April, 2017 |
|
|
|
Anthony Fox, Magnus Myreen, Yong Kiam Tan and Ramana Kumar Verified compilation of CakeML to multiple machine-code targets International Conference on Certified Programs and Proofs, pp. 125–137, Paris, France, January, 2017 |
|
|
|
Yong Kiam Tan, Magnus Myreen, Ramana Kumar, Anthony Fox, Scott Owens and Michael Norrish A new verified compiler backend for CakeML International Conference on Functional Programming, pp. 14, Nara, Japan, September, 2016 |
|
|
|
Yong Kiam Tan, Scott Owens and Ramana Kumar A verified type system for CakeML Implementation and application of functional and programming languages, pp. 12, Koblenz, Germany, July, 2016 Winner: 2016 Peter Landin Prize for best paper |