BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:An Overview of the CakeML verified compiler and some new challenge
 s - Thomas Sewell
DTSTART:20200306T100000Z
DTEND:20200306T102000Z
UID:TALK140377@talks.cam.ac.uk
CONTACT:Jean Pichon-Pharabod
DESCRIPTION:The CakeML project has developed a self-hosting verified compi
 ler for a language in the ML family. I've joined the project recently\, an
 d have been working on dynamic code execution. I'll give an overview of th
 e compiler design and proof design\, and discuss why dynamic code (Eval) i
 ntroduces some new and old challenges.
LOCATION:Computer Lab\, FW26
END:VEVENT
END:VCALENDAR