Mon 15 Jul 2019 13:30 - 14:30 at Epernay - Session Two

CakeML is an impure functional programming language aimed at supporting formally verified programs. The CakeML project has several aspects including formal semantics and metatheory, a verified compiler, a mechanised connection between its semantics and higher-order logic (in the HOL4 interactive theorem prover), and an example verified theorem prover written in CakeML and HOL4. It also has respectable performance compared to industrial-strength implementations of ML.

The CakeML project has been running for six years and has achieved its initial goal of demonstrating the feasibility of a practical, mechanically verified compiler from program source text to target machine code. But where should we go from here? In this talk, I will present an overview of the compiler, and the techniques we used to verify it. I will also present some example applications which have been built atop CakeML, and speculate on the role that a verified compiler can play in building trustworthy software.

Mon 15 Jul

FTfJP-2019-papers
13:30 - 15:00: FTfJP 2019 - Session Two at Epernay
FTfJP-2019-papers13:30 - 14:30
Talk
Scott OwensUniversity of Kent, UK
FTfJP-2019-papers14:30 - 15:00
Full-paper
Julia BelyakovaNortheastern University, USA
DOI Pre-print