BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:CakeML: A Verified Implementation of ML - Ramana Kumar (University
  of Cambridge)
DTSTART:20131203T130000Z
DTEND:20131203T140000Z
UID:TALK48734@talks.cam.ac.uk
CONTACT:William Denman
DESCRIPTION:(A practice talk for POPL 2014. 25 mins max.)\n\nWe have verif
 ied and bootstrapped a compiler for a large subset of standard ML. The res
 ulting system\, CakeML\, is a read-eval-print loop implemented in x86-64 m
 achine code and proved correct (in higher-order logic) with respect to our
  semantics for ML and for x86-64.\n\nThis is the first verification of com
 piler bootstrapping\, which we use to automate much of the synthesis and v
 erification of the compiler's implementation in machine code. The verifica
 tion depends on a tiny trusted code base (a HOL proof checker)\, and cover
 s lexing\, parsing\, type inference\, dynamic and incremental compilation\
 , garbage collection and bignum arithmetic. We have proved semantics-prese
 rvation including divergence-preservation. For the latter we use a novel l
 ightweight method based on logical timeouts.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR