A unification of graded and substructural logics

TL;DR

GRASS is a novel type system integrating graded and substructural logics, enabling flexible resource management and coexistence of multiple grade algebras within the same framework.

Contribution

It introduces GRASS, a unified type system that combines graded and substructural logics, allowing diverse resource control mechanisms and semantic integration of existing systems.

Findings

GRASS supports multiple grade algebras simultaneously.

Categorical semantics show GRASS subsumes systems like LNL, Adjoint Logic, and mGL.

The system enables flexible and modular resource-sensitive computation.

Abstract

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.