The Parallel Intensionally Fully Abstract Games Model of PCF

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 strategy that permits concurrent 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 Plot kin´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 intensionally fully abstract for PCF.