
arXiv: 2402.09138
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.
Submitted to Logical Methods in Computer Science
FOS: Computer and information sciences, Theory of computation → Linear logic, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], 000, Logic in Computer Science, Mathematics of computing → Partial differential equations, Theory of computation → Denotational semantics, Linear Logic, 004, Logic in Computer Science (cs.LO), Denotational Semantics, Graded Logic, Functional Analysis, ddc: ddc:004
FOS: Computer and information sciences, Theory of computation → Linear logic, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], 000, Logic in Computer Science, Mathematics of computing → Partial differential equations, Theory of computation → Denotational semantics, Linear Logic, 004, Logic in Computer Science (cs.LO), Denotational Semantics, Graded Logic, Functional Analysis, ddc: ddc:004
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
