We present a type theory combining both linearity and dependency by stratifying typing rules into a level for logics and a level for programs. The distinction between logics and programs decouples their semantics, allowing the type system to assume tight resource bounds. A natural notion of irrelevancy is established where all proofs and types occurring inside programs are fully erasable without compromising their operational behavior. Through a heap-based operational semantics, we show that extracted programs always make computational progress and run memory clean. Additionally, programs can be freely reflected into the logical level for conducting deep proofs in the style of standard dependent type theories. This enables one to write resource safe programs and verify their correctness using a unified language.

翻译：我们提出了一种结合线性与依赖性的类型理论，其类型规则被分层为逻辑层与程序层。逻辑与程序的区分解耦了二者的语义，使类型系统能够设定严格的资源界限。我们建立了一种自然的无关性概念：出现在程序内部的所有证明和类型均可完全擦除，而不会影响程序的操作行为。通过基于堆的操作语义，我们证明了所提取的程序始终能保持计算进展并以内存清洁的方式运行。此外，程序可自由反射至逻辑层，从而能以标准依赖类型理论风格进行深度证明。这使得我们能够使用统一语言编写资源安全的程序并验证其正确性。