Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Mirco A. Mannucci, Corey Thuro

TL;DR

The paper tackles the problem of certifying resource usage within typed programs by proposing a compositional type system that synthesizes resource bounds from an abstract lattice and checks them against budgets. It introduces a graded feasibility modality Box_r A and develops a syntactic term model in the presheaf topos Set^L, proving cost soundness, canonical forms, and initiality. The recursion-free simply-typed fragment is carefully analyzed with metatheory results (type and cost soundness) and a semantic justification via the Set^L model, while Lean 4 serves as an engineering focal point for recursion patterns and case studies such as binary search. The work enables modular reasoning about time, memory, and gas across multi-dimensional budgets, and provides a foundation for future mechanization, dependent types, and tooling, with practical impact on safety-critical and resource-bounded systems.

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.

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

TL;DR

The paper tackles the problem of certifying resource usage within typed programs by proposing a compositional type system that synthesizes resource bounds from an abstract lattice and checks them against budgets. It introduces a graded feasibility modality Box_r A and develops a syntactic term model in the presheaf topos Set^L, proving cost soundness, canonical forms, and initiality. The recursion-free simply-typed fragment is carefully analyzed with metatheory results (type and cost soundness) and a semantic justification via the Set^L model, while Lean 4 serves as an engineering focal point for recursion patterns and case studies such as binary search. The work enables modular reasoning about time, memory, and gas across multi-dimensional budgets, and provides a foundation for future mechanization, dependent types, and tooling, with practical impact on safety-critical and resource-bounded systems.

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.

Paper Structure

This paper contains 80 sections, 21 theorems, 10 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Goal (compositional resource bounds).
  3. Motivating Examples
  4. Contributions
  5. Scope of the Formalization
  6. Recursion patterns.
  7. Extensions beyond simple types.
  8. Design Principles
  9. Notation.
  10. A Minimal Calculus for Resource-Bounded Types
  11. Abstract Resource Lattices
  12. Examples.
  13. Core Typing Rules
  14. Reading the judgment.
  15. Three levels of cost.
  16. ...and 65 more sections

Key Result

Lemma 3.2

If $t \Downarrow v_1 \triangleright k_1$ and $t \Downarrow v_2 \triangleright k_2$, then $v_1 = v_2$ and $k_1 = k_2$.

Figures (2)

  • Figure 1: Core typing rules for recursion-free STLC with resource bounds. Constants $\delta_{\mathrm{app}}, \delta_{\mathrm{if}}, \delta_{\mathrm{unbox}} \in L$ are per-operation costs. The (Box) rule requires $b \preceq s$; the budget $r$ is independent and can be weakened. The (Lam) rule uses latent cost abstraction: the function carries its body cost $b$, paid upon application.
  • Figure 2: Big-step evaluation with cost. Values evaluate with cost $\bot$.

Theorems & Definitions (51)

  • Definition 3.1: Resource lattice
  • Lemma 3.2: Determinism
  • proof
  • Lemma 3.3: Typing substitution
  • proof
  • Lemma 3.4: Cost substitution
  • proof
  • Lemma 3.5: Budget weakening
  • proof
  • Theorem 3.6: Preservation
  • ...and 41 more