Resource-Bounded Martin-Löf Type Theory: Compositional Cost Analysis for Dependent Types
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866911378718064640 |
|---|---|
| author | Mannucci, Mirco A. Thuro, Corey |
| author_facet | Mannucci, Mirco A. Thuro, Corey |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2601_10772 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Resource-Bounded Martin-Löf Type Theory: Compositional Cost Analysis for Dependent Types Mannucci, Mirco A. Thuro, Corey Logic in Computer Science Computational Engineering, Finance, and Science Logic 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. |
| title | Resource-Bounded Martin-Löf Type Theory: Compositional Cost Analysis for Dependent Types |
| topic | Logic in Computer Science Computational Engineering, Finance, and Science Logic |
| url | https://arxiv.org/abs/2601.10772 |