BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Biorthogonality\, step-indexing and compiler correctness - Chung-K
 il Hur (University of Cambridge)
DTSTART:20090316T124500Z
DTEND:20090316T140000Z
UID:TALK17166@talks.cam.ac.uk
CONTACT:Sam Staton
DESCRIPTION:We define logical relations between the denotational semantics
  of a simply typed functional language with recursion and the operational 
 behaviour of low-level programs in a variant SECD machine. The relations\,
  which are defined using biorthogonality and step-indexing\, capture what 
 it means for a piece of low-level code to implement a mathematical\, domai
 n-theoretic function and are used to prove correctness of a simple compile
 r. The results have been formalized in the Coq proof assistant.\n\nThis is
  joint work with Nick Benton.
LOCATION:Room FW26\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR