Repository logo
 

The concurrent game semantics of Probabilistic PCF

Accepted version
Peer-reviewed

Type

Conference Object

Change log

Authors

Castellan, S 
Clairambault, P 
Paquet, H 
Winskel, G 

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.

Description

Keywords

46 Information and Computing Sciences, 4904 Pure Mathematics, 49 Mathematical Sciences, 50 Philosophy and Religious Studies, 5003 Philosophy

Journal Title

LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

Conference Name

33rd Annual ACM/IEEE Symposium on Logic in Computer Science

Journal ISSN

1043-6871

Volume Title

Publisher

Association for Computing Machinery

Rights

All rights reserved