Resource-Bounded Type Theory: Compositional Cost Analysis via Graded Modalities
Mirco A. Mannucci, Corey Thuro
cs.LO
Dec 7, 2025 · v1
TL;DR
Implements a resource-bounded binary search using Lean 4's well-founded recursion with separately proven logarithmic cost bounds.
Abstract
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 uniform treatment of time, memory, gas, and domain-specific costs. We introduce a graded feasibility modality with co-unit 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 a given budget, its operational cost is bounded by b. We provide a syntactic term model in the topos of presheaves over the lattice -- 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.
Problem
Formal methods typically certify what holds but not what it costs. In settings like safety-critical controllers, blockchain contracts, and time-bounded agents, a correct component that exceeds its resource envelope is unusable.
Approach
The authors present a compositional framework for certifying resource bounds in typed programs, where terms are typed with synthesized bounds from an abstract resource lattice. They introduce a graded feasibility modality with co-unit and monotonicity laws and prove a syntactic cost soundness theorem for the recursion-free simply-typed fragment. A syntactic term model in the topos of presheaves over the lattice is constructed, with cost extraction as a natural transformation. A case study demonstrates compositional reasoning for binary search using Lean's native recursion with separate bound proofs.
Results
The paper establishes initiality of the syntactic model (it embeds uniquely into all resource-bounded models), proves canonical forms via reification, and demonstrates the framework on binary search with compositional cost bounds in Lean.
