依赖性、成绩和伴随逻辑的结合
摘要：提议两种新的依赖类型系统：一种是依赖分级/线性类型系统，其中通过模态运算符将分级依赖类型系统与线性类型系统（Linear/Non-linear logic）连接起来。然后，通过引入Adjoint Logic中的模式（modes），我们将该系统推广为支持多个分级系统通过多个模态运算符连接的系统。最后，我们证明了这两个系统的几个元理论属性，包括分级代换（graded substitution）。
作者：Peter Hanukaev and Harley Eades III
论文ID：2307.09563
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-20