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

TL;DR

This paper introduces a compositional resource analysis framework for typed programs using graded modalities, enabling precise cost bounds for various resource types through a formal semantic model.

Contribution

It develops a novel graded feasibility modality and a syntactic cost soundness theorem, providing a formal foundation for resource-bound certification in typed programming languages.

Findings

Proves cost soundness for recursion-free simply-typed programs.

Constructs a syntactic model in the topos of presheaves over resource lattices.

Demonstrates compositional reasoning with a case study on binary search.

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.