Resource-Bounded Type Theory: Compositional Cost Analysis via Graded Modalities

Abstract

We present a compositional framework for certifying resource bounds in typed programs. Terms are typed with synthesized bounds b drawn from an abstract resource lattice (L, ⪯, ⊕, ⊔, ⊥), enabling uniform treatment of time, memory, gas, and domain-specific costs. We introduce a graded feasibility modality □ᵣ with counit and monotonicity laws. Our main result is a syntactic cost soundness theorem for the recursion-free simply-typed fragment: if a closed term has synthesized bound b under budget r, its operational cost is bounded by b. We provide a syntactic term model in the presheaf topos Setᴸ—where resource bounds index a cost-stratified family of definable values—with cost extraction as a natural transformation. We prove canonical forms via reification and establish initiality of the syntactic model: it embeds uniquely into all resource-bounded models. A case study demonstrates compositional reasoning for binary search using Lean’s native recursion with separate bound proofs.