TY - JOUR
TI - An introduction to Differential Linear Logic: proof-nets, models and antiderivatives
AU - Ehrhard, Thomas
T2 - arXiv:1606.01642 [cs]
AB - 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.
DA - 2016/06/06/
PY - 2016
DP - arXiv.org
ST - An introduction to Differential Linear Logic
UR - http://arxiv.org/abs/1606.01642
Y2 - 2019/11/28/11:52:31
KW - Denotational semantics
KW - Differential Linear Logic
KW - Differentiation
KW - Linear logic
ER -
TY - JOUR
TI - Differentials and distances in probabilistic coherence spaces
AU - Ehrhard, Thomas
T2 - arXiv:1902.04836 [cs]
AB - 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.
DA - 2019/02/13/
PY - 2019
DP - arXiv.org
UR - http://arxiv.org/abs/1902.04836
Y2 - 2019/11/28/11:57:10
KW - Coherence spaces
KW - Denotational semantics
KW - Differential Linear Logic
KW - Differentiation
KW - Linear logic
KW - Probabilistic programming
KW - Programming language theory
ER -
TY - JOUR
TI - Probabilistic coherence spaces as a model of higher-order probabilistic computation
AU - Ehrhard, Thomas
AU - Danos, Vincent
T2 - Information and Computation
AB - 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.
DA - 2011/06/01/
PY - 2011
DO - 10/ctfch6
DP - ScienceDirect
VL - 209
IS - 6
SP - 966
EP - 991
J2 - Information and Computation
LA - en
SN - 0890-5401
UR - http://www.sciencedirect.com/science/article/pii/S0890540111000411
Y2 - 2019/11/22/17:01:53
KW - Coherence spaces
KW - Probabilistic programming
KW - Programming language theory
KW - Semantics
ER -
TY - JOUR
TI - The differential lambda-calculus
AU - Ehrhard, Thomas
AU - Regnier, Laurent
T2 - Theoretical Computer Science
AB - We present an extension of the lambda-calculus with differential constructions. We state and prove some basic results (confluence, strong normalization in the typed case), and also a theorem relating the usual Taylor series of analysis to the linear head reduction of lambda-calculus.
DA - 2003/12/02/
PY - 2003
DO - 10/bf3b8v
DP - ScienceDirect
VL - 309
IS - 1
SP - 1
EP - 41
J2 - Theoretical Computer Science
LA - en
SN - 0304-3975
UR - http://www.sciencedirect.com/science/article/pii/S030439750300392X
Y2 - 2019/11/24/17:23:34
KW - Differentiation
KW - Linear logic
KW - Programming language theory
ER -
TY - JOUR
TI - Probabilistic call by push value
AU - Ehrhard, Thomas
AU - Tasson, Christine
T2 - arXiv:1607.04690 [cs]
AB - 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.
DA - 2018///
PY - 2018
DO - 10/ggdk8z
DP - arXiv.org
UR - http://arxiv.org/abs/1607.04690
Y2 - 2019/11/27/20:51:36
KW - Denotational semantics
KW - Linear logic
KW - Probabilistic programming
KW - Programming language theory
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 -
TY - JOUR
TI - A convenient differential category
AU - Blute, Richard
AU - Ehrhard, Thomas
AU - Tasson, Christine
T2 - arXiv:1006.3140 [cs, math]
AB - In this paper, we show that the category of Mackey-complete, separated, topological convex bornological vector spaces and bornological linear maps is a differential category. Such spaces were introduced by Fr\"olicher and Kriegl, where they were called convenient vector spaces. While much of the structure necessary to demonstrate this observation is already contained in Fr\"olicher and Kriegl's book, we here give a new interpretation of the category of convenient vector spaces as a model of the differential linear logic of Ehrhard and Regnier. Rather than base our proof on the abstract categorical structure presented by Fr\"olicher and Kriegl, we prefer to focus on the bornological structure of convenient vector spaces. We believe bornological structures will ultimately yield a wide variety of models of differential logics.
DA - 2010/06/16/
PY - 2010
DP - arXiv.org
UR - http://arxiv.org/abs/1006.3140
Y2 - 2019/11/28/18:10:01
KW - Differential Linear Logic
KW - Differentiation
KW - Linear logic
ER -
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 -