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

TL;DR

This paper extends Martin-Löf type theory with resource bounds, enabling certified size-dependent cost analysis of programs through a new universe hierarchy and graded modality, supported by semantic models and case studies.

Contribution

It introduces a resource-indexed universe hierarchy and graded modality in MLTT, providing a framework for certified cost bounds in dependent types, with semantic models and case studies.

Findings

Cost bounds over-approximate operational costs

Semantic model in presheaf topos extended with dependent presheaves

Canonicity and initiality results for the type theory

Abstract

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.