Higher-Order Distributions for Differential Linear Logic

Resource type
Authors/contributors
Title
Higher-Order Distributions for Differential Linear Logic
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.
Date
2019
Proceedings Title
Foundations of Software Science and Computation Structures
Place
Cham
Publisher
Springer International Publishing
Pages
330-347
Series
Lecture Notes in Computer Science
Language
en
DOI
10/ggdmrj
ISBN
978-3-030-17127-8
Library Catalog
Springer Link
Extra
ZSCC: NoCitationData[s1]
Citation
Kerjean, M., & Pacaud Lemay, J.-S. (2019). Higher-Order Distributions for Differential Linear Logic. In M. Bojańczyk & A. Simpson (Eds.), Foundations of Software Science and Computation Structures (pp. 330–347). Cham: Springer International Publishing. https://doi.org/10/ggdmrj
DIFFERENTIAL CALCULUS
Processing time: 0.02 seconds

Graph of references

(from Zotero to Gephi via Zotnet with this script)
Graph of references