USI - Email

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

Thursday

16.03

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

16:30 - 17:30


	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/

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