The concurrent game semantics of Probabilistic PCF

Simon Castellan, Pierre Clairambault, Hugo Paquet, Glynn Winskel

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

11 Citations (Scopus)
1 Downloads (Pure)

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.

Original languageEnglish
Title of host publicationProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
Place of PublicationNew York
Pages215-224
Number of pages10
DOIs
Publication statusPublished - 31 Jul 2018
Event33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018 - Oxford, United Kingdom
Duration: 9 Jul 201812 Jul 2018

Publication series

NameProceedings - Symposium on Logic in Computer Science
ISSN (Print)1043-6871

Conference

Conference33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
CountryUnited Kingdom
CityOxford
Period9/07/1812/07/18

Keywords

  • probabilistic PCF
  • probabilistic concurrent strategies
  • finite definability result

Fingerprint Dive into the research topics of 'The concurrent game semantics of Probabilistic PCF'. Together they form a unique fingerprint.

Cite this