TY - JOUR
TI - Measurable Cones and Stable, Measurable Functions
AU - Ehrhard, Thomas
AU - Pagani, Michele
AU - Tasson, Christine
T2 - Proceedings of the ACM on Programming Languages
AB - We define a notion of stable and measurable map between cones endowed with measurability tests and show that it forms a cpo-enriched cartesian closed category. This category gives a denotational model of an extension of PCF supporting the main primitives of probabilistic functional programming, like continuous and discrete probabilistic distributions, sampling, conditioning and full recursion. We prove the soundness and adequacy of this model with respect to a call-by-name operational semantics and give some examples of its denotations.
DA - 2017/12/27/
PY - 2017
DO - 10/ggdjf8
DP - arXiv.org
VL - 2
IS - POPL
SP - 1
EP - 28
J2 - Proc. ACM Program. Lang.
SN - 24751421
UR - http://arxiv.org/abs/1711.09640
Y2 - 2019/11/26/17:06:12
KW - Denotational semantics
KW - Probabilistic programming
KW - Programming language theory
ER -