Concurrent Hyland-Ong Games

Pierre Clairambault

This talk will be an overview of recent work in collaboration with Simon Castellan and Glynn Winskel on concurrent game semantics for higher-order programming languages.

In recent work, we have developed a new framework based on event structures for the game semantics of higher-order concurrent languages that avoids interleavings, and focuses on the causal structure of programs. In this talk I will give an overview of our work. I will first give a high-level description of the model, relying on examples from higher-order concurrent effectful languages (e.g. Idealized Parallel Algol -- IPA). Then I will describe two applications: firstly, a causal version of Ghica and Murawski's interleaving-based fully abstract games model of IPA. Secondly, a new interpretation of the sequential language PCF. Unlike the traditional one, the interpretation is parallel, and displays independent branches of computation. However, just as the traditional one, our model has a finite definability property and its extensional collapse is fully abstract.