@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}
}
@inproceedings{kerjean_higher-order_2019,
address = {Cham},
series = {Lecture {Notes} in {Computer} {Science}},
title = {Higher-{Order} {Distributions} for {Differential} {Linear} {Logic}},
isbn = {978-3-030-17127-8},
doi = {10/ggdmrj},
abstract = {Linear Logic was introduced as the computational counterpart of the algebraic notion of linearity. Differential Linear Logic refines Linear Logic with a proof-theoretical interpretation of the geometrical process of differentiation. In this article, we construct a polarized model of Differential Linear Logic satisfying computational constraints such as an interpretation for higher-order functions, as well as constraints inherited from physics such as a continuous interpretation for spaces. This extends what was done previously by Kerjean for first order Differential Linear Logic without promotion. Concretely, we follow the previous idea of interpreting the exponential of Differential Linear Logic as a space of higher-order distributions with compact-support, which is constructed as an inductive limit of spaces of distributions on Euclidean spaces. We prove that this exponential is endowed with a co-monadic like structure, with the notable exception that it is functorial only on isomorphisms. Interestingly, as previously argued by Ehrhard, this still allows the interpretation of differential linear logic without promotion.},
language = {en},
booktitle = {Foundations of {Software} {Science} and {Computation} {Structures}},
publisher = {Springer International Publishing},
author = {Kerjean, Marie and Pacaud Lemay, Jean-Simon},
editor = {Bojańczyk, Mikołaj and Simpson, Alex},
year = {2019},
note = {ZSCC: NoCitationData[s1]},
keywords = {Denotational semantics, Differential Linear Logic, Differentiation, Linear logic},
pages = {330--347}
}
@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}
}
@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{ehrhard_introduction_2016,
title = {An introduction to {Differential} {Linear} {Logic}: proof-nets, models and antiderivatives},
shorttitle = {An introduction to {Differential} {Linear} {Logic}},
url = {http://arxiv.org/abs/1606.01642},
abstract = {Differential Linear Logic enriches Linear Logic with additional logical rules for the exponential connectives, dual to the usual rules of dereliction, weakening and contraction. We present a proof-net syntax for Differential Linear Logic and a categorical axiomatization of its denotational models. We also introduce a simple categorical condition on these models under which a general antiderivative operation becomes available. Last we briefly describe the model of sets and relations and give a more detailed account of the model of finiteness spaces and linear and continuous functions.},
urldate = {2019-11-28},
journal = {arXiv:1606.01642 [cs]},
author = {Ehrhard, Thomas},
month = jun,
year = {2016},
note = {ZSCC: 0000002
arXiv: 1606.01642},
keywords = {Denotational semantics, Differential Linear Logic, Differentiation, Linear logic}
}
@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{keimel_predicate_2009,
title = {Predicate {Transformers} for {Extended} {Probability} and {Non}-determinism},
volume = {19},
issn = {0960-1295},
url = {http://dx.doi.org/10.1017/S0960129509007555},
doi = {10/bkvgqc},
abstract = {We investigate laws for predicate transformers for the combination of non-deterministic choice and (extended) probabilistic choice, where predicates are taken to be functions to the extended non-negative reals, or to closed intervals of such reals. These predicate transformers correspond to state transformers, which are functions to conical powerdomains, which are the appropriate powerdomains for the combined forms of non-determinism. As with standard powerdomains for non-deterministic choice, these come in three flavours – lower, upper and (order-)convex – so there are also three kinds of predicate transformers. In order to make the connection, the powerdomains are first characterised in terms of relevant classes of functionals. Much of the development is carried out at an abstract level, a kind of domain-theoretic functional analysis: one considers d-cones, which are dcpos equipped with a module structure over the non-negative extended reals, in place of topological vector spaces. Such a development still needs to be carried out for probabilistic choice per se; it would presumably be necessary to work with a notion of convex space rather than a cone.},
number = {3},
urldate = {2019-11-26},
journal = {Mathematical. Structures in Comp. Sci.},
author = {Keimel, Klaus and Plotkin, Gordon d.},
month = jun,
year = {2009},
note = {ZSCC: 0000015},
keywords = {Denotational semantics, Powerdomains, Programming language theory},
pages = {501--539}
}
@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{fiore_cartesian_2008,
title = {The cartesian closed bicategory of generalised species of structures},
volume = {77},
issn = {00246107},
url = {http://doi.wiley.com/10.1112/jlms/jdm096},
doi = {10/bd2mr9},
abstract = {The concept of generalised species of structures between small categories and, correspondingly, that of generalised analytic functor between presheaf categories are introduced. An operation of substitution for generalised species, which is the counterpart to the composition of generalised analytic functors, is also put forward. These deﬁnitions encompass most notions of combinatorial species considered in the literature—including of course Joyal’s original notion—together with their associated substitution operation. Our ﬁrst main result exhibits the substitution calculus of generalised species as arising from a Kleisli bicategory for a pseudo-comonad on profunctors. Our second main result establishes that the bicategory of generalised species of structures is cartesian closed.},
language = {en},
number = {1},
urldate = {2019-11-28},
journal = {Journal of the London Mathematical Society},
author = {Fiore, M. and Gambino, N. and Hyland, M. and Winskel, G.},
month = feb,
year = {2008},
note = {ZSCC: 0000067},
keywords = {Denotational semantics, Differential Linear Logic, Differentiation, Linear logic},
pages = {203--220}
}
@article{varacca_distributing_2006,
title = {Distributing probability over non-determinism},
volume = {16},
issn = {0960-1295, 1469-8072},
url = {http://www.journals.cambridge.org/abstract_S0960129505005074},
doi = {10/czs9sx},
language = {en},
number = {01},
urldate = {2019-11-26},
journal = {Mathematical Structures in Computer Science},
author = {Varacca, Daniele and Winskel, Glynn},
month = feb,
year = {2006},
note = {ZSCC: 0000108},
keywords = {Categorical probability theory, Denotational semantics, Programming language theory},
pages = {87}
}
@article{van_breugel_domain_2005,
series = {Foundations of {Software} {Science} and {Computation} {Structures}},
title = {Domain theory, testing and simulation for labelled {Markov} processes},
volume = {333},
issn = {0304-3975},
url = {http://www.sciencedirect.com/science/article/pii/S030439750400711X},
doi = {10/ft9vc5},
abstract = {This paper presents a fundamental study of similarity and bisimilarity for labelled Markov processes (LMPs). The main results characterize similarity as a testing preorder and bisimilarity as a testing equivalence. In general, LMPs are not required to satisfy a finite-branching condition—indeed the state space may be a continuum, with the transitions given by arbitrary probability measures. Nevertheless we show that to characterize bisimilarity it suffices to use finitely-branching labelled trees as tests. Our results involve an interaction between domain theory and measure theory. One of the main technical contributions is to show that a final object in a suitable category of LMPs can be constructed by solving a domain equation D≅V(D)Act, where V is the probabilistic powerdomain. Given an LMP whose state space is an analytic space, bisimilarity arises as the kernel of the unique map to the final LMP. We also show that the metric for approximate bisimilarity introduced by Desharnais, Gupta, Jagadeesan and Panangaden generates the Lawson topology on the domain D.},
language = {en},
number = {1},
urldate = {2019-11-26},
journal = {Theoretical Computer Science},
author = {van Breugel, Franck and Mislove, Michael and Ouaknine, Joël and Worrell, James},
month = mar,
year = {2005},
note = {ZSCC: 0000058},
keywords = {Coalgebras, Denotational semantics, Probabilistic transition systems, Transition systems},
pages = {171--197}
}
@article{desharnais_bisimulation_2002,
title = {Bisimulation for {Labelled} {Markov} {Processes}},
volume = {179},
issn = {0890-5401},
url = {http://www.sciencedirect.com/science/article/pii/S0890540101929621},
doi = {10/fmp9vd},
abstract = {In this paper we introduce a new class of labelled transition systems—labelled Markov processes— and define bisimulation for them. Labelled Markov processes are probabilistic labelled transition systems where the state space is not necessarily discrete. We assume that the state space is a certain type of common metric space called an analytic space. We show that our definition of probabilistic bisimulation generalizes the Larsen–Skou definition given for discrete systems. The formalism and mathematics is substantially different from the usual treatment of probabilistic process algebra. The main technical contribution of the paper is a logical characterization of probabilistic bisimulation. This study revealed some unexpected results, even for discrete probabilistic systems. •Bisimulation can be characterized by a very weak modal logic. The most striking feature is that one has no negation or any kind of negative proposition.•We do not need any finite branching assumption, yet there is no need of infinitary conjunction. We also show how to construct the maximal autobisimulation on a system. In the finite state case, this is just a state minimization construction. The proofs that we give are of an entirely different character than the typical proofs of these results. They use quite subtle facts about analytic spaces and appear, at first sight, to be entirely nonconstructive. Yet one can give an algorithm for deciding bisimilarity of finite state systems which constructs a formula that witnesses the failure of bisimulation.},
language = {en},
number = {2},
urldate = {2019-11-26},
journal = {Information and Computation},
author = {Desharnais, Josée and Edalat, Abbas and Panangaden, Prakash},
month = dec,
year = {2002},
note = {ZSCC: 0000297},
keywords = {Coalgebras, Denotational semantics, Probabilistic transition systems, Symbolic logic, Transition systems},
pages = {163--193}
}
@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}
}
@inproceedings{de_vink_bisimulation_1997,
address = {Berlin, Heidelberg},
series = {Lecture {Notes} in {Computer} {Science}},
title = {Bisimulation for probabilistic transition systems: {A} coalgebraic approach},
isbn = {978-3-540-69194-5},
shorttitle = {Bisimulation for probabilistic transition systems},
doi = {10/fcqzmk},
abstract = {The notion of bisimulation as proposed by Larsen and Skou for discrete probabilistic transition systems is shown to coincide with a coalgebraic definition in the sense of Aczel and Mendier in terms of a set functor. This coalgebraic formulation makes it possible to generalize the concepts to a continuous setting involving Borel probability measures. Under reasonable conditions, generalized probabilistic bisimilarity can be characterized categorically. Application of the final coalgebra paradigm then yields an internally fully abstract semantical domain with respect to probabilistic bisimulation.},
language = {en},
booktitle = {Automata, {Languages} and {Programming}},
publisher = {Springer},
author = {de Vink, E. P. and Rutten, J. J. M. M.},
editor = {Degano, Pierpaolo and Gorrieri, Roberto and Marchetti-Spaccamela, Alberto},
year = {1997},
note = {ZSCC: NoCitationData[s1]},
keywords = {Categorical probability theory, Coalgebras, Denotational semantics, Probabilistic transition systems, Transition systems},
pages = {460--470}
}
@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}
}
@inproceedings{jones_probabilistic_1989,
address = {Piscataway, NJ, USA},
title = {A {Probabilistic} {Powerdomain} of {Evaluations}},
isbn = {978-0-8186-1954-0},
url = {http://dl.acm.org/citation.cfm?id=77350.77370},
urldate = {2019-11-26},
booktitle = {Proceedings of the {Fourth} {Annual} {Symposium} on {Logic} in {Computer} {Science}},
publisher = {IEEE Press},
author = {Jones, C. and Plotkin, G.},
year = {1989},
note = {ZSCC: 0000389
event-place: Pacific Grove, California, USA},
keywords = {Denotational semantics, Powerdomains, Probabilistic programming, Programming language theory},
pages = {186--195}
}
@article{girard_linear_1987,
title = {Linear logic},
volume = {50},
issn = {0304-3975},
url = {http://www.sciencedirect.com/science/article/pii/0304397587900454},
doi = {10/cmv5mj},
abstract = {The familiar connective of negation is broken into two operations: linear negation which is the purely negative part of negation and the modality “of course” which has the meaning of a reaffirmation. Following this basic discovery, a completely new approach to the whole area between constructive logics and programmation is initiated.},
language = {en},
number = {1},
urldate = {2019-11-26},
journal = {Theoretical Computer Science},
author = {Girard, Jean-Yves},
month = jan,
year = {1987},
note = {ZSCC: 0005505},
keywords = {Denotational semantics, Linear logic, Type theory},
pages = {1--101}
}