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

Abstract

We extend resource-bounded type theory to Martin-Löf Type Theory (MLTT) withdependent types, enabling size-indexed cost bounds for programs over inductive families.Our calculus features dependent function types Πᵇ⁽ˣ⁾ₓ:ₐ B(x) where bounds b(x) depend on theargument, dependent pair types Σₓ:ₐB(x) with additive cost composition, and inductivefamilies (notably Vec(A, n) and Fin(n)) with structurally recursive eliminators carrying sizedependent bounds. We introduce a resource-indexed universe hierarchy Uᵣ where r ε L tracks the cost of type formation, and a graded modality □ᵣ for feasibility certification. Our main results are: (1) a cost soundness theorem establishing that synthesized bounds over-approximate operational costs, with bounds expressed as functions of size indices; (2)a semantic model in the presheaf topos Setᴸ extended with dependent presheaves and comprehension structure; (3) canonicity for the intensional fragment; and (4) initiality of the syntactic model. We demonstrate the framework with case studies including length-index edvector operations with O(n) bounds and binary search with O(log n) bounds 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.