Archive / INF Seminars / INF_2023_03_16_Magnus_OMyreen
USI - Email

The CakeML Project: Chasing End-to-End Correctness, Verified Compilation and Applications


Chair: Carlo Alberto Furia




USI Campus Est, room D0.03, Sector D // Online
16:30 - 17:30

Magnus O. Myreen
Chalmers University of Technology, Gothenburg, Sweden
This talk will be about the CakeML project. The CakeML project centres around an impure functional programming language, for which we have developed a collection of proofs and tools inside the HOL4 theorem prover. The development includes a proven-correct compiler that can bootstrap itself. This talk has two parts. In the first part, I will explain the research questions the CakeML project has tackled and outline the main research ideas that have helped us address them. The research questions include:
- how can we transfer properties proved of logic functions to properties of machine code compiled from those functions?
- how can we use a verified compiler to compile itself?
- how can we reason about space usage of CakeML programs?
- how can we prove liveness properties for non-terminating code?
In the second part, I will describe how the CakeML project strives to build meaningful connections with other projects and our experience with this so far. We have:
- built a proved-to-be-sound clone of the HOL light theorem prover
- produced a verified compiler for a Haskell-like language
- constructed several verified checkers, including checkers for UNSAT proofs, floating-point error bounds, OpenTheory article files, pseudo-Boolean proofs, and Integer Programming proofs
The CakeML project is an open project and we are always keen to explore new collaborations.
The CakeML webpage:
The CakeML project lives in the HOL4 theorem prover:

Magnus O. Myreen did his PhD in Cambridge UK during 2005-2008, supervised by Prof. Mike Gordon. After his PhD, he stayed on at Cambridge, first as a postdoc on his own grant and then as a Royal Society University Fellow. In 2014, he moved to Chalmers University of Technology, whereheI became a tenured Associate Professor in 2015.

Click here to join online: