Trustworthy Systems

CakeML

CakeML is a functional programming language with a proven-correct compiler.

Aim

Reducing the cost and increasing the guarantees of verified software.

Approach

Further information

See the CakeML project website.

People

Publications

These are publications involving Trustworthy Systems researchers. See the CakeML publications list for other publications.

Abstract PDF 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
plain text to be published 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
plain text to be published Arve Gengelbach and Johannes Åman Pohjola
A verified cyclicity checker: For theories with overloaded constants
Proceedings of the 13th International Conference on Interactive Theorem Proving, pp. 15:1–15:18, Haifa, Israel, August, 2022
plain text to be published Johannes Åman Pohjola, Alejandro Gómez-Londoño, James Shaker and Michael Norrish
Kalas: A verified, end-to-end compiler for a choreographic language
Proceedings of the 13th International Conference on Interactive Theorem Proving, pp. 27:1–27:18, Haifa, Israel, August, 2022
Abstract PDF
Presentation Video
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
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF Johannes Åman Pohjola, Henrik Rostedt and Magnus Myreen
Characteristic formulae for liveness properties of non-terminating CakeML programs
Proceedings of the 10th International Conference on Interactive Theorem Proving, pp. 32:1-19, Portland, Oregon, September, 2019
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF Alejandro Gomez-Londono and Johannes Åman Pohjola
Connecting choreography languages with verified stacks
at Nordic Workshop on Programming Theory, Oslo, Norway, October, 2018
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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
Abstract to be published 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
Abstract PDF 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
Abstract PDF 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
Abstract PDF 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