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 - JOUR
TI - Probabilistic coherence spaces as a model of higher-order probabilistic computation
AU - Ehrhard, Thomas
AU - Danos, Vincent
T2 - Information and Computation
AB - We study a probabilistic version of coherence spaces and show that these objects provide a model of linear logic. We build a model of the pure lambda-calculus in this setting and show how to interpret a probabilistic version of the functional language PCF. We give a probabilistic interpretation of the semantics of probabilistic PCF closed terms of ground type. Last we suggest a generalization of this approach, using Banach spaces.
DA - 2011/06/01/
PY - 2011
DO - 10/ctfch6
DP - ScienceDirect
VL - 209
IS - 6
SP - 966
EP - 991
J2 - Information and Computation
LA - en
SN - 0890-5401
UR - http://www.sciencedirect.com/science/article/pii/S0890540111000411
Y2 - 2019/11/22/17:01:53
KW - Coherence spaces
KW - Probabilistic programming
KW - Programming language theory
KW - Semantics
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 - JOUR
TI - Differentials and distances in probabilistic coherence spaces
AU - Ehrhard, Thomas
T2 - arXiv:1902.04836 [cs]
AB - In probabilistic coherence spaces, a denotational model of probabilistic functional languages, mor-phisms are analytic and therefore smooth. We explore two related applications of the corresponding derivatives. First we show how derivatives allow to compute the expectation of execution time in the weak head reduction of probabilistic PCF (pPCF). Next we apply a general notion of "local" differential of morphisms to the proof of a Lipschitz property of these morphisms allowing in turn to relate the observational distance on pPCF terms to a distance the model is naturally equipped with. This suggests that extending probabilistic programming languages with derivatives, in the spirit of the differential lambda-calculus, could be quite meaningful.
DA - 2019/02/13/
PY - 2019
DP - arXiv.org
UR - http://arxiv.org/abs/1902.04836
Y2 - 2019/11/28/11:57:10
KW - Coherence spaces
KW - Denotational semantics
KW - Differential Linear Logic
KW - Differentiation
KW - Linear logic
KW - Probabilistic programming
KW - Programming language theory
ER -