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