This paper presents preliminary work on a general system for integrating dependent types into substructural type systems such as linear logic and linear type theory. Prior work on this front has generally managed to deliver type systems possessing either syntax or semantics inclusive of certain practical applications, but has struggled to combine these all in one and the same system. Toward resolving this difficulty, I propose a novel categorical interpretation of substructural dependent types, analogous to the use of monoidal categories as models of linear and ordered logic, that encompasses a wide class of mathematical and computational examples. On this basis, I develop a general framework for substructural dependent type theories, and proceed to prove some essential metatheoretic properties thereof. As an application of this framework, I show how it can be used to construct a type theory that satisfactorily addresses the problem of effectively representing cut admissibility for linear sequent calculus in a logical framework.

翻译：本文提出了将依赖类型集成至子结构类型系统（如线性逻辑与线性类型理论）中通用系统的初步工作。此前在该方向上的研究虽然成功构建了兼具实用语法或语义的类型系统，但始终未能将两者统一于同一体系。为解决这一难题，我提出了一种新颖的范畴论解释方法，类比于使用幺半范畴作为线性逻辑与有序逻辑模型的方式，这种解释方法涵盖了广泛的数学与计算实例。在此基础上，我构建了子结构依赖类型理论的通用框架，并证明了其若干关键元理论性质。作为该框架的应用，我将展示如何利用它构建一种类型理论，从而在逻辑框架中妥善解决线性相继式演算的切割可容许性有效表示问题。