Campus Event Calendar
Event Entry
What and Who
The CakeML verified compiler
Scott Owens
University of Kent
SWS Colloquium
SWS, RG1, MMCI
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Thursday, 17 December 2015
13:00
90 Minutes
E1 5
029
Saarbrücken
Abstract
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 at NICTA, Magnus Myreen at
Chalmers, Michael Norrish at NICTA, Yong Kiam Tan at (A*STAR,
Singapore), and myself.
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 at NICTA, Magnus Myreen at
Chalmers, Michael Norrish at NICTA, Yong Kiam Tan at (A*STAR,
Singapore), and myself.
In this talk, I will explain the architecture of CakeML's verified
compiler, focussing
on a new optimising backend that we are currently developing.
CakeML's web site is https://cakeml.org, and development is hosted on GitHub at
https://github.com/CakeML/cakeml.
Contact
Claudia Richter
0681 9303 9103
--email hidden
passcode not visible
logged in users only
Claudia Richter, 12/09/2015 14:31 -- Created document.