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.

翻译：本文将资源受限类型理论扩展至具有依赖类型的马丁-洛夫类型理论（MLTT），实现了对归纳族上程序的规模索引代价界限分析。我们引入了资源索引的宇宙层级U_r（其中r属于L并追踪类型构造的代价）以及用于可行性验证的渐变模态Box_r。主要研究成果包括：（1）代价可靠性定理：证明所合成的界限是对操作代价的过近似，且界限可表示为规模索引的函数；（2）在L上的预层拓扑中构建语义模型，该模型通过依赖预层与理解结构进行扩展；（3）内涵片段的正规性定理；（4）语法模型的初始性。我们通过案例研究展示了该框架的实际应用，包括具有线性界限的长度索引向量操作与具有对数界限的二分搜索算法，二者均通过类型系统表达。本工作弥合了依赖类型理论与定量资源分析之间的鸿沟，为规模依赖算法提供了可验证的代价界限。