Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:A New Verified Compiler Backend for CakeML
Speaker:Magnus Myreen
coming from:Chalmers University of Technology, G├Âteborg
Speakers Bio: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.

Event Type:SWS Colloquium
Visibility:SWS, RG1, MMCI
We use this to send out email in the morning.
Level:AG Audience
Language:English
Date, Time and Location
Date:Wednesday, 22 February 2017
Time:10:30
Duration:90 Minutes
Location:Saarbr├╝cken
Building:E1 5
Room:029
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
Name(s):Annika Meiser
Phone:9303 9105
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:YesTo Location:Kaiserslautern
To Building:G26To Room:112
Meeting ID:
Tags, Category, Keywords and additional notes
Note:
Attachments, File(s):
  • Annika Meiser, 02/15/2017 01:47 PM -- Created document.