The concurrent game semantics of Probabilistic PCF
File(s)lics17.pdf (795.14 KB)
Accepted version
Author(s)
Castellan, SPA
Clairambault, Pierre
Paquet, Hugo
Winskel, Glynn
Type
Conference Paper
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 Issued
2018-07
Date Acceptance
2018-03-31
Citation
LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018, pp.215-224
Publisher
ACM
Start Page
215
End Page
224
Journal / Book Title
LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
Copyright Statement
© 2018 Copyright held by the owner/author(s). Publication rights licensed to Association for Computing Machinery.
Sponsor
Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (E
Grant Number
EP/K011715/1
ERI 025567 (EP/K034413/1)
Source
Symposium on Logic in Computer Science (LCIS 2018)
Publication Status
Published
Start Date
2018-07-09
Finish Date
2018-07-12
Coverage Spatial
Oxford, UK
Date Publish Online
2018-07-09