Simon Castellan (ENS Lyon), The parallel intensionally fully abstract model for PCF



In this talk, we introduce a new way to compose innocent strategies (a semantic representation of normal terms of PCF) based on the work of Rideau-Winskel on concurrent games on event structures.

This new framework can also deal with a notion of "concurrent innocent strategies" that can be composed and still form a model of PCF where term evaluation features some parallelism. We show that, similarly to Hyland and Ong's original construction, the quotient of this model by contextual equivalence is fully abstract for PCF, conveying the intuition that PCF terms cannot observe the fact that they are evaluated in parallel or sequentially.