Corey Thuro

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

2026 · Open MIND

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 …