TY - CONF
TI - The Geometry of Bayesian Programming
AU - Dal Lago, Ugo
AU - Hoshino, Naohiko
DA - 2019/06/01/
PY - 2019
DO - 10/ggdk85
DP - ResearchGate
SP - 1
EP - 13
KW - Bayesian inference
KW - Denotational semantics
KW - Linear logic
KW - Probabilistic programming
KW - Programming language theory
KW - Rewriting theory
KW - Transition systems
ER -
TY - CONF
TI - Higher-Order Distributions for Differential Linear Logic
AU - Kerjean, Marie
AU - Pacaud Lemay, Jean-Simon
A2 - Bojańczyk, Mikołaj
A2 - Simpson, Alex
T3 - Lecture Notes in Computer Science
AB - 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.
C1 - Cham
C3 - Foundations of Software Science and Computation Structures
DA - 2019///
PY - 2019
DO - 10/ggdmrj
DP - Springer Link
SP - 330
EP - 347
LA - en
PB - Springer International Publishing
SN - 978-3-030-17127-8
KW - Denotational semantics
KW - Differential Linear Logic
KW - Differentiation
KW - Linear logic
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 - 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 -