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
Current |
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 |