University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Fully Abstract Models of Call-by-Value Languages, à la O'Hearn & Riecke

Fully Abstract Models of Call-by-Value Languages, à la O'Hearn & Riecke

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Jamie Vicary.

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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2020 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity