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.

翻译：我们提出了两个新的依赖类型系统。第一个系统是一种依赖等级/线性类型系统，其中等级依赖类型系统通过模态算子连接到线性类型系统，该线性类型系统采用线性/非线性逻辑的风格。随后，我们将此系统推广，通过引入伴随逻辑中的模式，支持由多个模态算子连接的多个等级系统。最后，我们证明了这两个系统的若干元理论性质，包括等级替换。