一句话：将分级线性逻辑与微分线性逻辑统一，用微分算子幺半群索引指数连接词，并给出基于分布论的指称模型。
线性逻辑通过资源使用细化直觉主义逻辑，并已扩展出索引/分级线性逻辑和微分线性逻辑等方向。本文旨在统一这两个方向：首先把指数连接词用微分算子幺半群进行索引，定义微分版分级线性逻辑；随后证明它等价于有限微分线性逻辑的某个分级扩展。作者还基于分布论和常系数线性偏微分算子构造了指称模型，为该逻辑提供语义基础。该工作连接资源敏感分析与证明线性化，并为分级与微分线性逻辑提供统一框架。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2402-09138,
title = {Unifying Graded Linear Logic and Differential Operators},
author = {Flavien Breuvart and Marie Kerjean and Simon Mirwasser},
journal = {Logical Methods in Computer Science},
volume = {Volume 22, Issue 1},
year = {2026},
doi = {10.46298/lmcs-22(1:7)2026}
}