Combining dependency, grades, and adjoint logic

TL;DR

The paper introduces two novel dependent type systems that integrate graded, linear, and adjoint logic modalities, enabling advanced reasoning about resource management and logical modalities.

Contribution

It presents the first dependent graded/linear type system connected via modal operators and generalizes it using modes from Adjoint Logic, with formal meta-theoretic properties proven.

Findings

Established graded substitution property

Developed a generalized modal framework for dependent types

Proved meta-theoretic properties of the new systems

Abstract

We propose two new dependent type systems. The first, is a dependent graded/linear type system where a graded dependent type system is connected via modal operators to a linear type system in the style of Linear/Non-linear logic. We then generalize this system to support many graded systems connected by many modal operators through the introduction of modes from Adjoint Logic. Finally, we prove several meta-theoretic properties of these two systems including graded substitution.