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

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

• Philip Saville, University of Edinburgh
• Friday 20 November 2020, 14:00-15:00
• Online.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• Online
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.