Resource-Bounded Type Theory: Compositional Cost Analysis via Graded Modalities
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911306518364160 |
|---|---|
| author | Mannucci, Mirco A. Thuro, Corey |
| author_facet | Mannucci, Mirco A. Thuro, Corey |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_06952 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Resource-Bounded Type Theory: Compositional Cost Analysis via Graded Modalities Mannucci, Mirco A. Thuro, Corey Logic in Computer Science Computational Engineering, Finance, and Science Logic 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. |
| title | Resource-Bounded Type Theory: Compositional Cost Analysis via Graded Modalities |
| topic | Logic in Computer Science Computational Engineering, Finance, and Science Logic |
| url | https://arxiv.org/abs/2512.06952 |