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

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)x:A B(x) where bounds b(x) depend on theargument, dependent pair types ?x:AB(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 Ur where r ? Ltracks the cost of type formation, and a graded modality ?r for feasibility certification.Our main results are: (1) a cost soundness theorem establishing that synthesized boundsover-approximate operational costs, with bounds expressed as functions of size indices; (2)a semantic model in the presheaf topos SetLextended with dependent presheaves andcomprehension structure; (3) canonicity for the intensional fragment; and (4) initiality of thesyntactic model. We demonstrate the framework with case studies including length-indexedvector operations with O(n) bounds and binary search with O(log n) bounds expressed in thetype. This work bridges the gap between dependent type theory and quantitative resourceanalysis, enabling certified cost bounds for size-dependent algorithms.