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}$.

It can be used as a type system for tracking function sensitivity (types are then interpreted in the cateogry of metric spaces and short maps; see Reed & Pierce 2010 and Arthur Azevedo de Amorim et al. 2017) or information flow? (see Liepelt et al. 2025).

Graded linear logic can be seen as a simple (structural) coeffect? system.

Literature

• Jason Reed and Benjamin C. Pierce, Distance Makes the Types Grow Stronger, ICFP’10 [pdf]
• 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)
• Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata & Ikram Cherigui, A semantic account of metric preservation, POPL’17 (2017) [doi]
• 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]
• Vilem-Benjamin Liepelt, Danielle Marshall, Dominic Orchard, Vineet Rajani & Michael Vollmer, LNCS 15500 (2025) [doi]