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

Speaker: Magnus O. Myreen, Chalmers University of Technology, Gothenburg, Sweden

Abstract:
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: https://cakeml.org 
The CakeML project lives in the HOL4 theorem prover: https://hol-theorem-prover.org

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. https://www.cse.chalmers.se/~myreen/

Chair: Carlo Alberto Furia

Click here to join online: https://tinyurl.com/22r2p4us