Pierre Clairambault (LIP, CNRS et ENS Lyon)

The parallel intentionally fully abstract games model of PCF

Abstract: We describe a framework for truly concurrent game semantics of programming languages, based on Rideau and Winskel’s concurrent games on event structures. The model supports a notion of innocent strategies that permits concur- rent and non-deterministic behaviour, but which coincides with traditional Hyland-Ong innocent strategies if one restricts to the deterministic sequential case. In this framework we give an alternative interpretation of Plotkin’s PCF, that takes advantage of the concurrent nature of strategies and formalizes the idea that although PCF is a sequential language, certain sub-computations are independent and can be computed in a parallel fashion. We show that just as Hyland and Ong’s sequential interpretation of PCF, our parallel interpretation yields a model that is intentionally fully abstract for PCF. (this is a joint work with Simon Castellan and Glynn Winskel)