The concurrent game semantics of Probabilistic PCF

Resource type
Authors/contributors
Title
The concurrent game semantics of Probabilistic PCF
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.
Date
2018
Proceedings Title
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science - LICS '18
Conference Name
the 33rd Annual ACM/IEEE Symposium
Place
Oxford, United Kingdom
Publisher
ACM Press
Pages
215-224
Language
en
DOI
10/ggdjfz
ISBN
978-1-4503-5583-4
Accessed
2019-11-26T16:57:36Z
Library Catalog
Crossref
Extra
ZSCC: 0000018
Citation
Castellan, S., Clairambault, P., Paquet, H., & Winskel, G. (2018). The concurrent game semantics of Probabilistic PCF. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science - LICS ’18 (pp. 215–224). Oxford, United Kingdom: ACM Press. https://doi.org/10/ggdjfz
Processing time: 0.02 seconds

Graph of references

(from Zotero to Gephi via Zotnet with this script)
Graph of references