BCS FACS - The Cake ML verified compiler - an evening Seminar with Dr. Scott Owens

Date/Time: Thursday 25 September 2014, 6.00pm
Networking and refreshments will be available from 5.15pm.

Venue: BCS, 1st Floor, The Davidson Building, 5 Southampton Street, London, WC2E 7HA | Maps

Cost to attend: Free of charge

Speaker: Dr Scott Owens School of Computing, University of Kent


CakeML is a new ML dialect aimed at supporting formally verified programs.

The CakeML project has several aspects including formal semantics and metatheory, a verified compiler, a formal connection between its semantics and higher-order logic (in the HOL4 interactive theorem prover), and example verified applications written in CakeML and HOL4.

The project is an active collaboration between Ramana Kumar and Magnus Myreen at Cambridge, Michael Norrish at NICTA, and myself.

In this talk, I will explain the architecture of CakeML's verified compiler, and then show how we move verified functions from a theorem prover to CakeML (including bootstrapping the compiler itself).

Lastly, I will explain how these tools will allow us to support -- with a very small trusted computing base -- a verified version of the HOL Light theorem prover.

CakeML's website is https://cakeml.org, and development is hosted on GitHub at https://github.com/CakeML/cakeml.