Taylor expansion as a monad in models of DiLL

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.