FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
The concurrent game semantics of Probabilistic PCF

Authors: Simon Castellan, Pierre Clairambault, Hugo Paquet and Glynn Winskel

Paper Information

Title:The concurrent game semantics of Probabilistic PCF
Authors:Simon Castellan, Pierre Clairambault, Hugo Paquet and Glynn Winskel
Proceedings:LICS PDF files
Editors: Anuj Dawar and Erich Grädel
Keywords:Game semantics, Probabilistic programs, Concurrent games, Event structures
Abstract:

ABSTRACT. We define a new games model of Probabilistic PCF (PPCF) by enriching thin concurrent games with symmetry, recently introduced by Castellan et al, with probability. This model supports two interpretations of PPCF, one sequential and one parallel. We make the case for this model by exploiting the causal structure of probabilistic concurrent strategies. First, we show that the strategies obtained from PPCF programs have a deadlock-free interaction, and therefore deduce that there is an interpretation-preserving functor from our games to the probabilistic relational model recently proved fully abstract by Ehrhard et al. It follows that our model is intensionally fully abstract. Finally, we propose a definition of probabilistic innocence and prove a finite definability result, leading to a second (independent) proof of full abstraction.

Pages:10
Talk:Jul 10 16:20 (Session 57C)
Paper: