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 - 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 - 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 - COMP
TI - dmurfet/deeplinearlogic
AU - Murfet, Daniel
AB - Deep learning and linear logic. Contribute to dmurfet/deeplinearlogic development by creating an account on GitHub.
DA - 2018/07/14/T01:08:44Z
PY - 2018
DP - GitHub
LA - Jupyter Notebook
UR - https://github.com/dmurfet/deeplinearlogic
Y2 - 2019/11/22/16:44:43
KW - Categorical ML
KW - Implementation
KW - Linear logic
KW - Machine learning
KW - Semantics
ER -
TY - COMP
TI - dmurfet/polysemantics
AU - Murfet, Daniel
AB - Polynomial semantics of linear logic. Contribute to dmurfet/polysemantics development by creating an account on GitHub.
DA - 2018/04/29/T20:41:43Z
PY - 2018
DP - GitHub
LA - Python
UR - https://github.com/dmurfet/polysemantics
Y2 - 2019/11/22/16:45:35
KW - Categorical ML
KW - Implementation
KW - Linear logic
KW - Machine learning
KW - Semantics
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 - 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 - The cartesian closed bicategory of generalised species of structures
AU - Fiore, M.
AU - Gambino, N.
AU - Hyland, M.
AU - Winskel, G.
T2 - Journal of the London Mathematical Society
AB - 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.
DA - 2008/02//
PY - 2008
DO - 10/bd2mr9
DP - Crossref
VL - 77
IS - 1
SP - 203
EP - 220
LA - en
SN - 00246107
UR - http://doi.wiley.com/10.1112/jlms/jdm096
Y2 - 2019/11/28/16:31:36
KW - Denotational semantics
KW - Differential Linear Logic
KW - Differentiation
KW - Linear logic
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 - Linear logic
AU - Girard, Jean-Yves
T2 - Theoretical Computer Science
AB - 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.
DA - 1987/01/01/
PY - 1987
DO - 10/cmv5mj
DP - ScienceDirect
VL - 50
IS - 1
SP - 1
EP - 101
J2 - Theoretical Computer Science
LA - en
SN - 0304-3975
UR - http://www.sciencedirect.com/science/article/pii/0304397587900454
Y2 - 2019/11/26/21:07:06
KW - Denotational semantics
KW - Linear logic
KW - Type theory
ER -
TY - SLIDE
TI - Linear logic and deep learning
A2 - Murfet, Daniel
A2 - Hu, Huiyi
LA - en
KW - Categorical ML
KW - Linear logic
KW - Machine learning
KW - Semantics
ER -