BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Fully Abstract Models of Call-by-Value Languages\, à la O'Hearn &
 amp\; Riecke - Philip Saville\, University of Edinburgh
DTSTART:20201120T140000Z
DTEND:20201120T150000Z
UID:TALK152599@talks.cam.ac.uk
CONTACT:Jamie Vicary
DESCRIPTION:https://us02web.zoom.us/j/177472153?pwd=MFgwd0EzY05QSGtpSDc2dU
 16aG9wdz09\n\nPlotkin famously observed that the classical domains model f
 or PCF is\nnot fully abstract: there exist contextually equivalent PCF ter
 ms\nwith different semantic interpretations. It is a kind of\nfolklore tha
 t the problem of constructing fully abstract models for\nPCF lay open for 
 twenty years\, before being resolved by the\ngames-semantics approaches of
  Hyland & Ong and Abramsky &\nJagadeesan. What is less well-known\, howeve
 r\, is that at roughly the\nsame time O'Hearn and Riecke presented a fully
  abstract model which\n'refines' the domains model with logical relations.
 \n\nIn this talk I will present a categorical treatment of O'Hearn and\nRi
 ecke's construction. Starting with a suitable model of a\ncall-by-value la
 nguage in the style of Moggi's computational lambda\ncalculus\, I will out
 line how one can construct a fully abstract\nmodel. The construction uses 
 logical relations to cut out junk\, and so\ndoes not require any kind of q
 uotient.\n\nThis is joint work with Ohad Kammar.
LOCATION:Online
END:VEVENT
END:VCALENDAR