BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Realizability and Parametricity in Pure Type Systems: An applicati
 on - Jean-Philippe Bernardy\, University of Gothenburg
DTSTART:20101123T111500Z
DTEND:20101123T121500Z
UID:TALK28023@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:We describe a systematic method to build a logic from any prog
 ramming language described as a Pure Type System (PTS). The formulas of th
 is logic express properties about programs. We define a parametricity theo
 ry about programs and a realizability theory for the logic. The logic is e
 xpressive enough to internalize both theories. Thanks to the PTS setting\,
  we abstract most idiosyncrasies specific to particular type theories. Thi
 s confers generality to the results\, and reveals parallels between parame
 tricity and realizability. The red-thread of the talk will be a possible i
 mplication on the design of programming languages featuring dependent type
 s.
LOCATION:Small lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR