A Two-Level Linear Dependent Type Theory

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 semantics to be independently tailored to suit the needs of theorem proving and programming. 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 without the need for runtime garbage collection. Additionally, programs can be freely lifted 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.