Linear Logic refines Intuitionnistic Logic by taking into account the resources used during the proof and program computation. In the past decades, it has been extended to various frameworks. The most famous are indexed linear logics which can describe the resource management or the complexity analysis of a program. From an other perspective, Differential Linear Logic is an extension which allows the linearization of proofs. In this article, we merge these two directions by first defining a differential version of Graded linear logic: this is made by indexing exponential connectives with a monoid of differential operators. We prove that it is equivalent to a graded version of previously defined extension of finitary differential linear logic. We give a denotational model of our logic, based on distribution theory and linear partial differential operators with constant coefficients.

Differentiation in logic has several sources of inspiration. The most recent is differentiable programming, models of which demand functoriality and good typing properties. More historical is reverse denotational semantics, taking inspiration from models of Linear Logic to differentiate proofs and λ-terms. In this paper, we take advantage of the rich structure of categorical models of Linear Logic to give a new functorial presentation of differentiation. We define differentiation as a functor from a coslice of the category of smooth maps to the category of linear maps. Extending linear-non-linear adjunction models of Linear Logic, this produces models of Differential Linear Logic. We use these functorial presentations to shed new light on integration in differential categories.

In a differential category and in Differential Linear Logic, the exponential conjunction ! admits structural maps, characterizing quantitative operations and symmetric co-structural maps, characterizing differentiation. In this paper, we introduce the notion of a Laplace distributor, which is an extra structural map which distributes the linear negation operation (_)^∗ over ! and transforms the co-structural rules into the structural rules. Laplace distributors are directly inspired by the well-known Laplace transform, which is all-important in numerical analysis. In the star-autonomous setting, a Laplace distributor induces a natural transformation from ! to the exponential disjunction ?, which we then call a Laplace transformation. According to its semantics, we show that Laplace distributors correspond precisely to the notion of a generalized exponential function e^x on the monoidal unit. We also show that many well-known and important examples have a Laplace distributor/transformation, including (weighted) relations, finiteness spaces, Köthe spaces, and convenient vector spaces.

Automatic Differentiation is the study of the efficient computation of differentials. While the first automatic differentiation algorithms are concomitant with the birth of computer science, the specific backpropagation algorithm has been brought to a modern light by its application to neural networks. This work unveils a surprising connection between backpropagation and Gödel's Dialectica interpretation, a logical translation that realizes semi-classical axioms. This unexpected correspondence is exploited through different logical settings. In particular, we show that the computational interpretation of Dialectica translates to the differential λ-calculus and that Differential Linear Logic subsumes the logical interpretation of Dialectica.

Differential Linear Logic (DiLL) adds to Linear Logic (LL) a symmetrization of three out of the four exponential rules, which allows the expression of a natural notion of differentiation. In this paper, we introduce a codigging inference rule for DiLL and study the categorical semantics of DiLL with codigging using differential categories. The addition of codigging makes the rules of DiLL completely symmetrical. We will explain how codigging is interpreted thanks to the exponential function ex, and in certain cases by the convolutional exponential. In a setting with codigging, every proof is equal to its Taylor series, which implies that every model of DiLL with codigging is quantitative. We provide examples of codigging in relational models, as well as models related to game logic and quantum programming. We also construct a graded model of DiLL with codigging in which the indices witness exponential growth. Codigging makes the exponential of-course connective ! in LL into a monad, where the monad axioms enforce Taylor expansion. As such, codigging opens the door to monadic reformulations of quantitative features in programming languages, as well as further categorical generalizations.

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.

Differential Linear Logic (DiLL), introduced by Ehrhard and Regnier, extends linear logic with a notion of linear approximation of proofs. While DiLL is classical logic, i.e. has an involutive negation, classical denotational models of it in which this notion of differentiation corresponds to the usual one, defined on any smooth function, were missing. We solve this issue by constructing a model of it based on nuclear topological vector spaces and distributions with compact support.

In this paper, we describe a denotational model of Intuitionist Linear Logic which is also a differential category. Formulas are interpreted as Mackey-complete topological vector space and linear proofs are interpreted as bounded linear functions. So as to interpret non-linear proofs of Linear Logic, we use a notion of power series between Mackey-complete spaces, generalizing entire functions in $\mathbb{C}$ . Finally, we get a quantitative model of Intuitionist Differential Linear Logic, with usual syntactic differentiation and where interpretations of proofs decompose as a Taylor expansion.