一句话：为 DiLL 引入 codigging 规则，证明 ! 在范畴语义中构成单子，且每条证明等于其泰勒展开，模型因此定量。
微分线性逻辑（DiLL）通过对称化指数规则中的三条，使线性逻辑能够表达微分。本文为 DiLL 引入 codigging 推理规则，使指数规则完全对称，并借助 differential categories 研究其范畴语义。作者用指数函数 ex 解释 codigging，在特定情形下用卷积指数解释；证明含 codigging 时每条证明都等于其泰勒级数，因此每个模型都是定量的。文章给出关系模型、博弈逻辑与量子编程相关模型中的实例，并构造分级模型，其中指标见证指数增长。关键结论是 of-course 模态 ! 成为单子，其单子公理强制泰勒展开，从而开启编程语言中定量特征的单子式重构与范畴推广。
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.