@article{baudart_reactive_2019,
title = {Reactive {Probabilistic} {Programming}},
url = {http://arxiv.org/abs/1908.07563},
abstract = {Synchronous reactive languages were introduced for designing and implementing real-time control software. These domain-specific languages allow for writing a modular and mathematically precise specification of the system, enabling a user to simulate, test, verify, and, finally, compile the system into executable code. However, to date these languages have had limited modern support for modeling uncertainty -- probabilistic aspects of the software's environment or behavior -- even though modeling uncertainty is a primary activity when designing a control system. In this paper we extend Z{\textbackslash}'elus, a synchronous programming language, to deliver ProbZ{\textbackslash}'elus, the first synchronous probabilistic programming language. ProbZ{\textbackslash}'elus is a probabilistic programming language in that it provides facilities for probabilistic models and inference: inferring latent model parameters from data. We present ProbZ{\textbackslash}'elus's measure-theoretic semantics in the setting of probabilistic, stateful stream functions. We then demonstrate a semantics-preserving compilation strategy to a first-order functional core calculus that lends itself to a simple semantic presentation of ProbZ{\textbackslash}'elus's inference algorithms. We also redesign the delayed sampling inference algorithm to provide bounded and streaming delayed sampling inference for ProbZ{\textbackslash}'elus models. Together with our evaluation on several reactive programs, our results demonstrate that ProbZ{\textbackslash}'elus provides efficient, bounded memory probabilistic inference.},
urldate = {2019-11-28},
journal = {arXiv:1908.07563 [cs]},
author = {Baudart, Guillaume and Mandel, Louis and Atkinson, Eric and Sherman, Benjamin and Pouzet, Marc and Carbin, Michael},
month = aug,
year = {2019},
note = {ZSCC: 0000001
arXiv: 1908.07563},
keywords = {Bayesian inference, Denotational semantics, Implementation, Probabilistic programming, Programming language theory}
}
@article{ehrhard_differentials_2019,
title = {Differentials and distances in probabilistic coherence spaces},
url = {http://arxiv.org/abs/1902.04836},
abstract = {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.},
urldate = {2019-11-28},
journal = {arXiv:1902.04836 [cs]},
author = {Ehrhard, Thomas},
month = feb,
year = {2019},
note = {ZSCC: 0000000
arXiv: 1902.04836},
keywords = {Coherence spaces, Denotational semantics, Differential Linear Logic, Differentiation, Linear logic, Probabilistic programming, Programming language theory}
}
@article{ehrhard_probabilistic_2018,
title = {Probabilistic call by push value},
url = {http://arxiv.org/abs/1607.04690},
doi = {10/ggdk8z},
abstract = {We introduce a probabilistic extension of Levy's Call-By-Push-Value. This extension consists simply in adding a " flipping coin " boolean closed atomic expression. This language can be understood as a major generalization of Scott's PCF encompassing both call-by-name and call-by-value and featuring recursive (possibly lazy) data types. We interpret the language in the previously introduced denotational model of probabilistic coherence spaces, a categorical model of full classical Linear Logic, interpreting data types as coalgebras for the resource comonad. We prove adequacy and full abstraction, generalizing earlier results to a much more realistic and powerful programming language.},
urldate = {2019-11-27},
journal = {arXiv:1607.04690 [cs]},
author = {Ehrhard, Thomas and Tasson, Christine},
year = {2018},
note = {ZSCC: 0000013[s0]
arXiv: 1607.04690},
keywords = {Denotational semantics, Linear logic, Probabilistic programming, Programming language theory}
}
@article{ehrhard_measurable_2017,
title = {Measurable {Cones} and {Stable}, {Measurable} {Functions}},
volume = {2},
issn = {24751421},
url = {http://arxiv.org/abs/1711.09640},
doi = {10/ggdjf8},
abstract = {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.},
number = {POPL},
urldate = {2019-11-26},
journal = {Proceedings of the ACM on Programming Languages},
author = {Ehrhard, Thomas and Pagani, Michele and Tasson, Christine},
month = dec,
year = {2017},
note = {ZSCC: 0000021
arXiv: 1711.09640},
keywords = {Denotational semantics, Probabilistic programming, Programming language theory},
pages = {1--28}
}
@article{keimel_mixed_2017,
title = {Mixed powerdomains for probability and nondeterminism},
url = {http://arxiv.org/abs/1612.01005},
doi = {10/ggdmrp},
abstract = {We consider mixed powerdomains combining ordinary nondeterminism and probabilistic nondeterminism. We characterise them as free algebras for suitable (in)equation-al theories; we establish functional representation theorems; and we show equivalencies between state transformers and appropriately healthy predicate transformers. The extended nonnegative reals serve as `truth-values'. As usual with powerdomains, everything comes in three flavours: lower, upper, and order-convex. The powerdomains are suitable convex sets of subprobability valuations, corresponding to resolving nondeterministic choice before probabilistic choice. Algebraically this corresponds to the probabilistic choice operator distributing over the nondeterministic choice operator. (An alternative approach to combining the two forms of nondeterminism would be to resolve probabilistic choice first, arriving at a domain-theoretic version of random sets. However, as we also show, the algebraic approach then runs into difficulties.) Rather than working directly with valuations, we take a domain-theoretic functional-analytic approach, employing domain-theoretic abstract convex sets called Kegelspitzen; these are equivalent to the abstract probabilistic algebras of Graham and Jones, but are more convenient to work with. So we define power Kegelspitzen, and consider free algebras, functional representations, and predicate transformers. To do so we make use of previous work on domain-theoretic cones (d-cones), with the bridge between the two of them being provided by a free d-cone construction on Kegelspitzen.},
urldate = {2019-11-28},
journal = {arXiv:1612.01005 [cs]},
author = {Keimel, Klaus and Plotkin, Gordon D.},
year = {2017},
note = {ZSCC: 0000001
arXiv: 1612.01005},
keywords = {Denotational semantics, Powerdomains, Probabilistic programming, Programming language theory}
}
@article{staton_semantics_2016,
title = {Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints},
shorttitle = {Semantics for probabilistic programming},
url = {http://arxiv.org/abs/1601.04943},
doi = {10/ggdf97},
abstract = {We study the semantic foundation of expressive probabilistic programming languages, that support higher-order functions, continuous distributions, and soft constraints (such as Anglican, Church, and Venture). We define a metalanguage (an idealised version of Anglican) for probabilistic computation with the above features, develop both operational and denotational semantics, and prove soundness, adequacy, and termination. They involve measure theory, stochastic labelled transition systems, and functor categories, but admit intuitive computational readings, one of which views sampled random variables as dynamically allocated read-only variables. We apply our semantics to validate nontrivial equations underlying the correctness of certain compiler optimisations and inference algorithms such as sequential Monte Carlo simulation. The language enables defining probability distributions on higher-order functions, and we study their properties.},
urldate = {2019-11-23},
journal = {Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science - LICS '16},
author = {Staton, Sam and Yang, Hongseok and Heunen, Chris and Kammar, Ohad and Wood, Frank},
year = {2016},
note = {ZSCC: 0000071
arXiv: 1601.04943},
keywords = {Bayesianism, Probabilistic programming, Programming language theory, Semantics},
pages = {525--534}
}
@article{ehrhard_probabilistic_2011,
title = {Probabilistic coherence spaces as a model of higher-order probabilistic computation},
volume = {209},
issn = {0890-5401},
url = {http://www.sciencedirect.com/science/article/pii/S0890540111000411},
doi = {10/ctfch6},
abstract = {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.},
language = {en},
number = {6},
urldate = {2019-11-22},
journal = {Information and Computation},
author = {Ehrhard, Thomas and Danos, Vincent},
month = jun,
year = {2011},
note = {ZSCC: 0000065},
keywords = {Coherence spaces, Probabilistic programming, Programming language theory, Semantics},
pages = {966--991}
}
@article{tix_semantic_2009,
title = {Semantic {Domains} for {Combining} {Probability} and {Non}-{Determinism}},
volume = {222},
issn = {15710661},
url = {https://linkinghub.elsevier.com/retrieve/pii/S1571066109000036},
doi = {10/d9hwq7},
abstract = {We present domain-theoretic models that support both probabilistic and nondeterministic choice. In [36], Morgan and McIver developed an ad hoc semantics for a simple imperative language with both probabilistic and nondeterministic choice operators over a discrete state space, using domain-theoretic tools. We present a model also using domain theory in the sense of D.S. Scott (see e.g. [15]), but built over quite general continuous domains instead of discrete state spaces.},
language = {en},
urldate = {2019-11-26},
journal = {Electronic Notes in Theoretical Computer Science},
author = {Tix, Regina and Keimel, Klaus and Plotkin, Gordon},
month = feb,
year = {2009},
note = {ZSCC: 0000055},
keywords = {Denotational semantics, Powerdomains, Probabilistic programming, Programming language theory},
pages = {3--99}
}
@article{jones_probabilistic_1989,
title = {Probabilistic {Non}-determinism},
language = {en},
author = {Jones, Claire},
year = {1989},
note = {ZSCC: 0000000},
keywords = {Denotational semantics, Probabilistic programming, Programming language theory},
pages = {198}
}