Write a Blog >>

Type-theoretic frameworks for complexity analysis are important for formulating complexity-theoretic arguments, and for automating runtime analysis. Choice of framework can have a large impact on both \emph{expressiveness}, the class of programs which the framework can reason about, and \emph{usability}, the degree to which the framework automates the analysis, or relies on user-created proofs. In this work, we describe a framework for complexity analysis in which the runtime of language-internal terms can be evaluated and reasoned about. Our framework provides both a high level of usability by automating the calculation of exact runtimes and runtime recurrences, and a high level of expressiveness with its ability to reason about all programs expressible in the calculus of constructions. The runtime of open terms is represented by atomic language constructs, enabling analysis of higher-order functions, and creating a compositional structure. Finally, we prove a faithfulness property, showing that all internally computed runtimes for closed terms correspond to their runtimes as defined by our language semantics.