@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}
}
@inproceedings{dal_lago_geometry_2019,
title = {The {Geometry} of {Bayesian} {Programming}},
doi = {10/ggdk85},
author = {Dal Lago, Ugo and Hoshino, Naohiko},
month = jun,
year = {2019},
note = {ZSCC: 0000000},
keywords = {Bayesian inference, Denotational semantics, Linear logic, Probabilistic programming, Programming language theory, Rewriting theory, Transition systems},
pages = {1--13}
}
@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}
}
@inproceedings{castellan_concurrent_2018,
address = {Oxford, United Kingdom},
title = {The concurrent game semantics of {Probabilistic} {PCF}},
isbn = {978-1-4503-5583-4},
url = {http://dl.acm.org/citation.cfm?doid=3209108.3209187},
doi = {10/ggdjfz},
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.},
language = {en},
urldate = {2019-11-26},
booktitle = {Proceedings of the 33rd {Annual} {ACM}/{IEEE} {Symposium} on {Logic} in {Computer} {Science} - {LICS} '18},
publisher = {ACM Press},
author = {Castellan, Simon and Clairambault, Pierre and Paquet, Hugo and Winskel, Glynn},
year = {2018},
note = {ZSCC: 0000018},
keywords = {Denotational semantics, Game semantics, Interactive semantics, Probabilistic programming, Programming language theory},
pages = {215--224}
}
@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}
}
@incollection{yang_commutative_2017,
address = {Berlin, Heidelberg},
title = {Commutative {Semantics} for {Probabilistic} {Programming}},
volume = {10201},
isbn = {978-3-662-54433-4 978-3-662-54434-1},
url = {http://link.springer.com/10.1007/978-3-662-54434-1_32},
abstract = {We show that a measure-based denotational semantics for probabilistic programming is commutative. The idea underlying probabilistic programming languages (Anglican, Church, Hakaru, ...) is that programs express statistical models as a combination of prior distributions and likelihood of observations. The product of prior and likelihood is an unnormalized posterior distribution, and the inference problem is to ﬁnd the normalizing constant. One common semantic perspective is thus that a probabilistic program is understood as an unnormalized posterior measure, in the sense of measure theory, and the normalizing constant is the measure of the entire semantic domain.},
language = {en},
urldate = {2019-11-23},
booktitle = {Programming {Languages} and {Systems}},
publisher = {Springer Berlin Heidelberg},
author = {Staton, Sam},
editor = {Yang, Hongseok},
year = {2017},
doi = {10.1007/978-3-662-54434-1_32},
note = {ZSCC: NoCitationData[s0] },
keywords = {Bayesianism, Probabilistic programming, Programming language theory, Semantics},
pages = {855--879}
}
@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}
}
@inproceedings{ehrhard_probabilistic_2014,
address = {San Diego, California, USA},
title = {Probabilistic coherence spaces are fully abstract for probabilistic {PCF}},
isbn = {978-1-4503-2544-8},
url = {http://dl.acm.org/citation.cfm?doid=2535838.2535865},
doi = {10/ggdf9x},
abstract = {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.},
language = {en},
urldate = {2019-11-22},
booktitle = {Proceedings of the 41st {ACM} {SIGPLAN}-{SIGACT} {Symposium} on {Principles} of {Programming} {Languages} - {POPL} '14},
publisher = {ACM Press},
author = {Ehrhard, Thomas and Tasson, Christine and Pagani, Michele},
year = {2014},
note = {ZSCC: 0000060},
keywords = {Coherence spaces, Probabilistic programming, Programming language theory, Semantics},
pages = {309--320}
}
@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}
}
@inproceedings{ehrhard_computational_2011,
address = {Toronto, ON, Canada},
title = {The {Computational} {Meaning} of {Probabilistic} {Coherence} {Spaces}},
isbn = {978-1-4577-0451-2},
url = {http://ieeexplore.ieee.org/document/5970206/},
doi = {10/cpv52n},
abstract = {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.},
language = {en},
urldate = {2019-11-26},
booktitle = {2011 {IEEE} 26th {Annual} {Symposium} on {Logic} in {Computer} {Science}},
publisher = {IEEE},
author = {Ehrhard, Thomas and Pagani, Michele and Tasson, Christine},
month = jun,
year = {2011},
note = {ZSCC: 0000036},
keywords = {Coherence spaces, Denotational semantics, Probabilistic programming, Programming language theory},
pages = {87--96}
}
@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}
}
@inproceedings{danos_probabilistic_2000,
title = {Probabilistic game semantics},
volume = {3},
isbn = {978-0-7695-0725-5},
doi = {10/b6k43s},
abstract = {A category of HO/N-style games and probabilistic strategies is developed where the possible choices of a strategy are quantified so as to give a measure of the likelihood of seeing a given play. A 2-sided die is shown to be universal in this category, in the sense that any strategy breaks down into a composition between some deterministic strategy and that die. The interpretative power of the category is then demonstrated by delineating a Cartesian closed subcategory which provides a fully abstract model of a probabilistic extension of Idealized Algol},
author = {Danos, Vincent and Harmer, Russell},
month = feb,
year = {2000},
note = {ZSCC: NoCitationData[s1]},
keywords = {Denotational semantics, Game semantics, Interactive semantics, Probabilistic programming, Programming language theory},
pages = {204--213}
}