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.

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