BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Compiling Functional Types to Relational Specifications for Low Le
 vel Imperative Code - Nick Benton
DTSTART:20081117T124500Z
DTEND:20081117T140000Z
UID:TALK14773@talks.cam.ac.uk
CONTACT:Matthew Parkinson
DESCRIPTION:We describe a semantic type soundness result\, formalized in t
 he Coq proof assistant\, for a compiler from a simple functional language 
 into an idealized assembly language. Types in the high-level language are 
 interpreted as binary relations\, built using both second-order quantifica
 tion and separation\, over stores and values in the low-level machine.\n\n
 This is joint work with Nicolas Tabareau from PPS\, Paris 7.
LOCATION:FW26
END:VEVENT
END:VCALENDAR