Abstract

https://us02web.zoom.us/j/177472153?pwd=MFgwd0EzY05QSGtpSDc2dU16aG9wdz09

Plotkin famously observed that the classical domains model for PCF is not fully abstract: there exist contextually equivalent PCF terms with different semantic interpretations. It is a kind of folklore that the problem of constructing fully abstract models for PCF lay open for twenty years, before being resolved by the games-semantics approaches of Hyland & Ong and Abramsky & Jagadeesan. What is less well-known, however, is that at roughly the same time O’Hearn and Riecke presented a fully abstract model which ‘refines’ the domains model with logical relations.

In this talk I will present a categorical treatment of O’Hearn and Riecke’s construction. Starting with a suitable model of a call-by-value language in the style of Moggi’s computational lambda calculus, I will outline how one can construct a fully abstract model. The construction uses logical relations to cut out junk, and so does not require any kind of quotient.

This is joint work with Ohad Kammar.