Skip to main content

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

CakeML is a collaborative effort by researchers at multiple institutions. At Data61, we have:

People

Publications

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

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 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: Theory, Tools and Experiments, pp. 88-111, Oxford, UK, November, 2018
Abstract PDF Adam Sandberg Ericsson, Magnus Myreen and Johannes Åman Pohjola
A verified generational garbage collector for CakeML
Journal of Automated Reasoning, 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 PDF Anthony Fox, Magnus Myreen, Yong Kiam Tan and Ramana Kumar
Verified compilation of CakeML to multiple machine-code targets
Certified Programs and Proofs 2017, 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
Served by Apache on Linux on seL4.