paperbot · PL 论文追踪

RSS

Unifying Graded Linear Logic and Differential Operators

LMCS vol.Volume 22, Issue 12026
Flavien Breuvart, Marie Kerjean, Simon Mirwasser

尚未生成 AI 速览(可能缺少 API key 或等待下次运行补跑)。

原文摘要(Abstract)

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 原文 ·

BibTeX
@article{paperbot4031,
  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}
}