BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Realizability Semantics of Parametric Polymorphism\, General Refer
 ences\, and Recursive Types - Lars Birkedal\, ITU Denmark
DTSTART:20081106T153000Z
DTEND:20081106T163000Z
UID:TALK15118@talks.cam.ac.uk
CONTACT:Matthew Parkinson
DESCRIPTION: We present a realizability model for a call-by-value\, higher
 -order\n programming language with parametric polymorphism\, general first
 -class\n references\, and recursive types.  The main novelty is a relation
 al\n interpretation of open types (as needed for parametricity reasoning) 
 that\n include general reference types.  The interpretation uses a new app
 roach\n to modeling references.\n\n The universe of semantic types consist
 s of world-indexed families of\n logical relations over a universal predom
 ain.  In order to model general\n reference types\, worlds are finite maps
  from locations to semantic types:\n this introduces a circularity between
  semantic types and worlds that\n precludes a direct definition of either.
   Our solution is to solve a\n recursive equation in an appropriate catego
 ry of metric spaces.  In\n effect\, types are interpreted using a Kripke l
 ogical relation over a\n recursively defined set of worlds.\n\nJoint work 
 with Kristian Stovring and Jacob Thamsborg
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR