结合依赖、分级与伴随逻辑
Combining dependency, grades, and adjoint logic
AI总结：
本研究提出两种新的依赖类型系统，先构建结合模态算子的依赖分级/线性类型系统，再引入伴随逻辑的模式实现多分级系统多模态连接，并证明其包括分级替换在内的元理论性质。
摘要：
我们提出两种新的依赖类型系统。第一种是依赖分级/线性类型系统，其中分级依赖类型系统通过模态算子，以线性/非线性逻辑的风格与线性类型系统相连。随后我们推广该系统，通过引入伴随逻辑（Adjoint Logic）的模式，支持由多个模态算子连接的多个分级系统。最后，我们证明了这两种系统的若干元理论性质，包括分级替换。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
