Type systems which account for resource sensitive computations can generally be split into two styles: First, substructural logics such as Linear Logic which seek to restrict weakening and contraction and reintroduce them in a controlled manner; And second, graded systems which allow weakening and contraction by default, but track the use of variables quantitatively in some algebraic structure -- usually a semiring. We present GRASS (Graded and substructural), a type system which incorporates mechanisms from both of these approaches, thus allowing maximally flexible control over variable usage. Furthermore, GRASS allows grades from an arbitrary collection of grade algebras to coexist in the same system, thus allowing different variables to be controlled with respect to different notions of resource within the same program. We develop the categorical semantics of \gyaru{}, and find that, on the level of categorical semantics, it subsumes multiple established systems such as LNL, Adjoint Logic, and mGL.

翻译：资源敏感计算的类型系统通常可分为两类：其一，以线性逻辑为代表的子结构逻辑，旨在限制弱化与收缩规则，并可控地重新引入它们；其二，分级系统默认允许弱化与收缩，但通过某种代数结构（通常是半环）定量追踪变量的使用。我们提出GRASS（分级与子结构）类型系统，融合了上述两种方法，从而实现对变量使用的最大灵活控制。此外，GRASS允许来自任意分级代数集合的等级在同一系统中共存，使得可基于不同资源概念在同一程序中控制不同变量。我们发展了GRASS的范畴语义，并发现其在范畴语义层面上涵盖了LNL、伴随逻辑与mGL等多个现有系统。