Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Resource-Bounded Martin-Löf Type Theory: Compositional Cost Analysis for Dependent Types

Mirco A. Mannucci, Corey Thuro

TL;DR

The paper addresses certified cost analysis for dependent type theories by extending resource-bounded type theory to Martin-Löf Type Theory (MLTT) with dependent types and size-indexed cost bounds. It introduces a resource-indexed universe $\mathcal{U}_r$ and a graded modality $\Box_r$, develops a presheaf-based semantic model over groupoids, and proves cost soundness, canonicity, and initiality. The authors demonstrate practical applicability through case studies on length-indexed vectors, binary search, and sorting, showing how bounds such as $O(1)$, $O(n)$, and $O(n\log n)$ can be certified directly in types. This work bridges dependent type theory and quantitative resource analysis, enabling certified, size-dependent cost bounds for algorithms expressed within dependent types and offering a foundation for future extensions to HoTT and automated bound synthesis.

Abstract

We extend resource-bounded type theory to Martin-Lof type theory (MLTT) with dependent types, enabling size-indexed cost bounds for programs over inductive families. We introduce a resource-indexed universe hierarchy U_r where r is an element of L and tracks the cost of type formation, and a graded modality Box_r for feasibility certification. Our main results are: (1) a cost soundness theorem showing that synthesized bounds over-approximate operational costs, with bounds expressed as functions of size indices; (2) a semantic model in the presheaf topos over L, extended with dependent presheaves and a comprehension structure; (3) canonicity for the intensional fragment; and (4) initiality of the syntactic model. We demonstrate the framework with case studies including length-indexed vector operations with linear bounds and binary search with logarithmic bounds, both expressed in the type. This work bridges the gap between dependent type theory and quantitative resource analysis, enabling certified cost bounds for size-dependent algorithms.

Resource-Bounded Martin-Löf Type Theory: Compositional Cost Analysis for Dependent Types

TL;DR

The paper addresses certified cost analysis for dependent type theories by extending resource-bounded type theory to Martin-Löf Type Theory (MLTT) with dependent types and size-indexed cost bounds. It introduces a resource-indexed universe and a graded modality , develops a presheaf-based semantic model over groupoids, and proves cost soundness, canonicity, and initiality. The authors demonstrate practical applicability through case studies on length-indexed vectors, binary search, and sorting, showing how bounds such as , , and can be certified directly in types. This work bridges dependent type theory and quantitative resource analysis, enabling certified, size-dependent cost bounds for algorithms expressed within dependent types and offering a foundation for future extensions to HoTT and automated bound synthesis.

Abstract

We extend resource-bounded type theory to Martin-Lof type theory (MLTT) with dependent types, enabling size-indexed cost bounds for programs over inductive families. We introduce a resource-indexed universe hierarchy U_r where r is an element of L and tracks the cost of type formation, and a graded modality Box_r for feasibility certification. Our main results are: (1) a cost soundness theorem showing that synthesized bounds over-approximate operational costs, with bounds expressed as functions of size indices; (2) a semantic model in the presheaf topos over L, extended with dependent presheaves and a comprehension structure; (3) canonicity for the intensional fragment; and (4) initiality of the syntactic model. We demonstrate the framework with case studies including length-indexed vector operations with linear bounds and binary search with logarithmic bounds, both expressed in the type. This work bridges the gap between dependent type theory and quantitative resource analysis, enabling certified cost bounds for size-dependent algorithms.
Paper Structure (94 sections, 15 theorems, 27 equations)

This paper contains 94 sections, 15 theorems, 27 equations.

Table of Contents

  1. Introduction
  2. Motivating example.
  3. Contributions.
  4. Scope.
  5. Relation to Prior Work
  6. Design Principles
  7. Notation.
  8. Resource-Bounded MLTT: The Calculus
  9. Judgments
  10. Contexts
  11. Universes
  12. Dependent Function Types ($\Pi$-types)
  13. Key insight.
  14. Non-dependent case.
  15. Dependent Pair Types ($\Sigma$-types)
  16. ...and 79 more sections

Key Result

Proposition 3.6

If we restrict RB--MLTT to: and we read a judgement $\Gamma \vdash_{r;\,b} t : A$ as an RB--TT typing judgement with grade $b$, then the typing rules of RB--MLTT reduce to those of RB--TT. Moreover, the operational cost semantics and soundness theorem specialize to the corresponding results in mannucci2025rbtt.

Theorems & Definitions (55)

  • Remark 3.1: Role of the ambient budget
  • Definition 3.2: Resource-indexed universes
  • Definition 3.3: Dependent function type with bounds
  • Definition 3.4: $\mathsf{Vec}(A, n)$
  • Example 3.5: Safe vector lookup
  • Proposition 3.6: RB--TT fragment
  • proof : Proof sketch
  • Definition 4.1: Bound language
  • Example 4.2: Common bound patterns
  • Example 4.3: Vector sum with linear bound
  • ...and 45 more