2 papers
cs.LO2026
Resource-Bounded Martin-Löf Type Theory: Compositional Cost Analysis for Dependent Types
Mirco A. Mannucci, Corey Thuro
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…
cs.LO2025
Resource-Bounded Type Theory: Compositional Cost Analysis via Graded Modalities
Mirco A. Mannucci, Corey Thuro
We present a compositional framework for certifying resource bounds in typed programs. Terms are typed with synthesized bounds drawn from an abstract resource lattice, enabling uni…