nLab graded linear logic

Idea

Graded linear logic can refer to multiple extensions of bounded linear logic, but most notably to $\mathrm{B}_\mathcal{S}\mathrm{LL}$, where the exponentials are indexed by elements of a semiring $\mathcal{S}$.

Literature

• Dan Ghica and Alex I. Smith, Bounded linear types in a resource semiring, Programming Languages and Systems (2014)
• Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic, A core quantitative coeffect calculus, Programming Languages and Systems (2014)
• Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Flavien Breuvart, and Tarmo Uustalu, Combining effects and coeffects via grading, ACM SIGPLAN International Conference on Functional Programming (2016)
• Dominic Orchard, Vilem-Benjamin Liepelt and Harley Eades III, Quantitative Program Reasoning with Graded Modal Types (2019) [pdf]
• Yōji Fukihara and Shin-ya Katsumata, Generalized bounded linear logic and its categorical semantics, Foundations of Software Science and Computation Structure (2021)
• Flavien Breuvart, Marie Kerjean and Simon Mirwasser, Unifying Graded Linear Logic and Differential Operators, International Conference on Formal Structures for Computation and Deduction (2023) [pdf]