arXiv subjects

Corey Thuro

Publications and source records attributed to Corey Thuro.

2 recordsLinked to original sources

arXiv2026

Resource-Bounded Martin-L\"of Type Theory: Compositional Cost Analysis for Dependent Types

We extend resource-bounded type theory to Martin-Lof type theory (MLTT) with dependent types, enabling size-indexed cost bounds for programs over inductive families. We introduce a resource-indexed universe hierarchy U_r where r is an element of L and tracks the cost of type formation, and a graded modality Box_r for feasibility certification. Our main results are: (1) a cost soundness theorem showing that synthesized bounds over-approximate operational costs, with bounds expressed as functions of size indices; (2) a semantic model in the presheaf topos over L, extended with dependent presheaves and a comprehension structure; (3) canonicity for the intensional fragment; and (4) initiality of the syntactic model. We demonstrate the framework with case studies including length-indexed vector operations with linear bounds and binary search with logarithmic bounds, both expressed in the type. This work bridges the gap between dependent type theory and quantitative resource analysis, enabling certified cost bounds for size-dependent algorithms.

cs.LO↗

arXiv2025

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

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.

cs.LO↗