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

Decanato - Facoltà di scienze informatiche

Data: 16 Marzo 2023 / 16:30 - 17:30

USI Campus Est, room D0.03, Sector D // Online

Speaker: 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:

Biography: 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.

Chair: Carlo Alberto Furia

Click here to join online: