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 - Differential Structure in Models of Multiplicative Biadditive Intuitionistic Linear Logic
AU - Fiore, Marcelo P.
A2 - Della Rocca, Simona Ronchi
T3 - Lecture Notes in Computer Science
AB - In the first part of the paper I investigate categorical models of multiplicative biadditive intuitionistic linear logic, and note that in them some surprising coherence laws arise. The thesis for the second part of the paper is that these models provide the right framework for investigating differential structure in the context of linear logic. Consequently, within this setting, I introduce a notion of creation operator (as considered by physicists for bosonic Fock space in the context of quantum field theory), provide an equivalent description of creation operators in terms of creation maps, and show that they induce a differential operator satisfying all the basic laws of differentiation (the product and chain rules, the commutation relations, etc.).
C1 - Berlin, Heidelberg
C3 - Typed Lambda Calculi and Applications
DA - 2007///
PY - 2007
DO - 10/c8vgx8
DP - Springer Link
SP - 163
EP - 177
LA - en
PB - Springer
SN - 978-3-540-73228-0
KW - Differential Linear Logic
KW - Differentiation
KW - Linear logic
ER -
TY - CONF
TI - On Geometry of Interaction
AU - Girard, Jean-Yves
A2 - Schwichtenberg, Helmut
T3 - NATO ASI Series
AB - The paper expounds geometry of interaction, for the first time in the full case, i.e. for all connectives of linear logic, including additives and constants. The interpretation is done within a C*-algebra which is induced by the rule of resolution of logic programming, and therefore the execution formula can be presented as a simple logic programming loop. Part of the data is public (shared channels) but part of it can be viewed as private dialect (defined up to isomorphism) that cannot be shared during interaction, thus illustrating the theme of communication without understanding. One can prove a nilpotency (i.e. termination) theorem for this semantics, and also its soundness w.r.t. a slight modification of familiar sequent calculus in the case of exponential-free conclusions.
C1 - Berlin, Heidelberg
C3 - Proof and Computation
DA - 1995///
PY - 1995
DO - 10/fr557p
DP - Springer Link
SP - 145
EP - 191
LA - en
PB - Springer
SN - 978-3-642-79361-5
KW - Interactive semantics
KW - Linear logic
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 -