{"id":"arxiv/2601.10772","url":"https://arxiv.org/abs/2601.10772","tags":["cs.LO","cs.CE","math.LO"],"score":0,"title":"Resource-Bounded Martin-Löf Type Theory: Compositional Cost Analysis for Dependent Types","domain":"cs.LO","source":"arxiv","authors":["Mirco A. Mannucci","Corey Thuro"],"reviews":0,"subject":"cs.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-01-15","reactions":{}}