TY - CONF
TI - The concurrent game semantics of Probabilistic PCF
AU - Castellan, Simon
AU - Clairambault, Pierre
AU - Paquet, Hugo
AU - Winskel, Glynn
T2 - the 33rd Annual ACM/IEEE Symposium
AB - 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.
C1 - Oxford, United Kingdom
C3 - Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science - LICS '18
DA - 2018///
PY - 2018
DO - 10/ggdjfz
DP - Crossref
SP - 215
EP - 224
LA - en
PB - ACM Press
SN - 978-1-4503-5583-4
UR - http://dl.acm.org/citation.cfm?doid=3209108.3209187
Y2 - 2019/11/26/16:57:36
KW - Denotational semantics
KW - Game semantics
KW - Interactive semantics
KW - Probabilistic programming
KW - Programming language theory
ER -
TY - CONF
TI - Probabilistic coherence spaces are fully abstract for probabilistic PCF
AU - Ehrhard, Thomas
AU - Tasson, Christine
AU - Pagani, Michele
T2 - the 41st ACM SIGPLAN-SIGACT Symposium
AB - Probabilistic coherence spaces (PCoh) yield a semantics of higherorder probabilistic computation, interpreting types as convex sets and programs as power series. We prove that the equality of interpretations in PCoh characterizes the operational indistinguishability of programs in PCF with a random primitive.
C1 - San Diego, California, USA
C3 - Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL '14
DA - 2014///
PY - 2014
DO - 10/ggdf9x
DP - Crossref
SP - 309
EP - 320
LA - en
PB - ACM Press
SN - 978-1-4503-2544-8
UR - http://dl.acm.org/citation.cfm?doid=2535838.2535865
Y2 - 2019/11/22/17:00:49
KW - Coherence spaces
KW - Probabilistic programming
KW - Programming language theory
KW - Semantics
ER -
TY - CONF
TI - The Computational Meaning of Probabilistic Coherence Spaces
AU - Ehrhard, Thomas
AU - Pagani, Michele
AU - Tasson, Christine
T2 - 2011 26th Annual IEEE Symposium on Logic in Computer Science (LICS 2011)
AB - We study the probabilistic coherent spaces — a denotational semantics interpreting programs by power series with non negative real coefﬁcients. We prove that this semantics is adequate for a probabilistic extension of the untyped λ-calculus: the probability that a term reduces to a head normal form is equal to its denotation computed on a suitable set of values. The result gives, in a probabilistic setting, a quantitative reﬁnement to the adequacy of Scott’s model for untyped λ-calculus.
C1 - Toronto, ON, Canada
C3 - 2011 IEEE 26th Annual Symposium on Logic in Computer Science
DA - 2011/06//
PY - 2011
DO - 10/cpv52n
DP - Crossref
SP - 87
EP - 96
LA - en
PB - IEEE
SN - 978-1-4577-0451-2
UR - http://ieeexplore.ieee.org/document/5970206/
Y2 - 2019/11/26/20:50:00
KW - Coherence spaces
KW - Denotational semantics
KW - Probabilistic programming
KW - Programming language theory
ER -
TY - CONF
TI - A Probabilistic Powerdomain of Evaluations
AU - Jones, C.
AU - Plotkin, G.
C1 - Piscataway, NJ, USA
C3 - Proceedings of the Fourth Annual Symposium on Logic in Computer Science
DA - 1989///
PY - 1989
DP - ACM Digital Library
SP - 186
EP - 195
PB - IEEE Press
SN - 978-0-8186-1954-0
UR - http://dl.acm.org/citation.cfm?id=77350.77370
Y2 - 2019/11/26/17:27:23
KW - Denotational semantics
KW - Powerdomains
KW - Probabilistic programming
KW - Programming language theory
ER -