BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A new verified compiler backend for CakeML - Magnus Myreen\, Chalm
 ers University\, Sweden
DTSTART:20160818T140000Z
DTEND:20160818T150000Z
UID:TALK67103@talks.cam.ac.uk
CONTACT:Dominic Mulligan
DESCRIPTION:This talk will give an overview of the CakeML project and in p
 articular report on a new compiler backend.\n\nCakeML is a strict function
 al programming language in the style of Standard ML and OCaml. It has a ve
 rified implementation with verified parsing\, type inference\, and compila
 tion.\n\nWe have recently developed and mechanically verified a new compil
 er backend for CakeML. Our new compiler features a sequence of intermediat
 e languages that allows it to incrementally compile away high-level featur
 es and enables verification at the right levels of semantic detail. In thi
 s way\, it resembles mainstream (unverified) compilers for strict function
 al languages. The compiler supports efficient curried multi-argument funct
 ions\, configurable data representations\, exceptions that unwind the call
  stack\, register allocation\, and more. The compiler targets several arch
 itectures: x86-64\, ARMv6\, ARMv8\, MIPS-64\, and RISC-V.\n\nI will talk a
 bout the overall structure of the compiler\, including its 12 intermediate
  languages\, and explain how everything fits together. The talk focus part
 icularly on the interaction between the verification of the register alloc
 ator and the garbage collector\, and memory representations.\n\nThe CakeML
  project (https://cakeml.org/) is a collaboration between people at Data61
  (Australia)\, Cambridge (UK)\, IHPC (Singapore)\, \nKent (UK) and Chalmer
 s (Sweden).
LOCATION:FW11
END:VEVENT
END:VCALENDAR