MPI-INF Logo
Campus Event Calendar

Event Entry

What and Who

A New Verified Compiler Backend for CakeML

Magnus Myreen
Chalmers University of Technology, Göteborg
SWS Colloquium

I grew up in Finland, but did my undergraduate studies in Oxford UK where Dr Jeff Sanders was my tutor. I completed my PhD on verification of
machine-code programs in 2009 at the University of Cambridge UK supervised by Prof. Mike Gordon. My PhD dissertation was selected as the
winner of the BCS Distinguished Dissertation Competition in 2010. In 2012, I became a Royal Society Research Fellow. In 2014, I moved to
Chalmers, where I became Associate Professor (tenured) in 2015.
SWS, RG1, MMCI  
AG Audience
English

Date, Time and Location

Wednesday, 22 February 2017
10:30
90 Minutes
E1 5
029
Saarbrücken

Abstract

The CakeML project has recently produced a verified compiler which we believe to be the most realistic verified compiler for a functional
programming language to date. In this talk I'll give an overview of the CakeML project with focus on the new compiler, in particular how
the compiler is structured, how the intermediate languages are designed and how the proofs are carried out. The talk will stay at a
fairly high-level, but I am happy to dive into details for any of the parts that I know well.

The CakeML project is currently a collaboration between six sites across three continents. The new compiler is due to: Anthony Fox
(Cambridge, UK), Ramana Kumar (Data61, Sydney Australia), Magnus Myreen (Chalmers, Sweden), Michael Norrish (Data61, Canberra
Australia), Scott Owens (Kent, UK), and Yong Kiam Tan (CMU, USA).

Contact

Annika Meiser
9303 9105
--email hidden

Video Broadcast

Yes
Kaiserslautern
G26
112
passcode not visible
logged in users only

Annika Meiser, 02/15/2017 13:47 -- Created document.