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:The CakeML verified compiler
Speaker:Scott Owens
coming from:University of Kent
Speakers Bio:
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:Thursday, 17 December 2015
Time:13:00
Duration:90 Minutes
Location:Saarbr├╝cken
Building:E1 5
Room:029
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.

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
Name(s):Claudia Richter
Phone:0681 9303 9103
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Note:
Attachments, File(s):

Created by:Claudia Richter/MPI-SWS, 12/09/2015 02:27 PMLast modified by:Uwe Brahm/MPII/DE, 11/24/2016 04:13 PM
  • Claudia Richter, 12/09/2015 02:31 PM -- Created document.