BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:POSTPONED:   Abstract machines and certified compilers - Maciej Pi
 róg
DTSTART:20150917T090000Z
DTEND:20150917T100000Z
UID:TALK60891@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:A compiler is called _certified_ if it comes with a machine-ve
 rified proof of its correctness with respect to the semantics of the sourc
 e and target languages. In am going to talk about certified compilers for 
 high-level languages with non-trivial semantics\, such as the lazy semanti
 cs of Haskell\, and how systematic manipulation of semantics can guide the
  design of such a compiler\, or even automatise the process.
LOCATION:FW26
END:VEVENT
END:VCALENDAR