Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Two-Level Linear Dependent Type Theory

Qiancheng Fu, Hongwei Xi

TL;DR

The paper presents TLL, a two-level linear dependent type theory that separates logic from programs to track resources precisely while allowing proofs to be erased. It develops a rigorous erasure procedure and a heap semantics to ensure extracted programs run with memory safety, and provides meta-theoretic results (confluence, normalization, subject reduction) formalized in Coq with an OCaml compiler producing C code. By reflecting program-level terms into the logical level, it achieves code sharing between fragments and supports sort-polymorphism and linear inductive types. This work offers a unified framework for writing resource-safe programs and verifying their correctness, with practical tooling and clear avenues for future extensions.

Abstract

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.

A Two-Level Linear Dependent Type Theory

TL;DR

The paper presents TLL, a two-level linear dependent type theory that separates logic from programs to track resources precisely while allowing proofs to be erased. It develops a rigorous erasure procedure and a heap semantics to ensure extracted programs run with memory safety, and provides meta-theoretic results (confluence, normalization, subject reduction) formalized in Coq with an OCaml compiler producing C code. By reflecting program-level terms into the logical level, it achieves code sharing between fragments and supports sort-polymorphism and linear inductive types. This work offers a unified framework for writing resource-safe programs and verifying their correctness, with practical tooling and clear avenues for future extensions.

Abstract

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.
Paper Structure (38 sections, 21 theorems, 7 equations, 40 figures)

This paper contains 38 sections, 21 theorems, 7 equations, 40 figures.

Table of Contents

  1. Introduction
  2. Overall Structure
  3. Logical Typing
  4. Type Formation
  5. Logical Terms
  6. Program Typing
  7. Program Context
  8. Context Management
  9. General Typing
  10. Irrelevance Quantification
  11. Relevance Quantification
  12. Program Extraction
  13. General Extraction
  14. Irrelevance Erasure
  15. Relevance Erasure
  16. ...and 23 more sections

Key Result

Theorem 1

If ${m \leadsto^{*} m_{1}}$ and ${m \leadsto^{*} m_{2}}$, then there exists $n$ such that ${m_{1} \leadsto^{*} n}$ and ${m_{2} \leadsto^{*} n}$.

Figures (40)

  • Figure 1: Logical and Program Typing
  • Figure 2: Syntax of TLL
  • Figure 3: Logical Context
  • Figure 4: Type Formation
  • Figure 5: Logical Terms
  • ...and 35 more figures

Theorems & Definitions (21)

  • Theorem 1: Confluence of Logical Reductions
  • Theorem 2: Type Validity
  • Theorem 3: Sort Uniqueness
  • Theorem 4: Logical Subject Reduction
  • Lemma 1: Logical Type Model
  • Lemma 2: Logical Reduction Model
  • Theorem 5: Logical Strong Normalization
  • Lemma 3: Program 0-Weakening
  • Lemma 4: Program 1-Weakening
  • Theorem 6: Program Reflection
  • ...and 11 more