A static cost analysis for a higher-order language

TL;DR

This paper introduces a static complexity analysis for a higher-order functional language, providing certified upper bounds on evaluation costs through formal proof in Coq.

Contribution

It presents a novel static analysis framework for higher-order languages with structural recursion, including a formal proof of soundness in Coq.

Findings

Provides a translation function mapping expressions to complexities

Establishes that the complexity bounds are sound and formalized in Coq

Offers a method to compute certified upper bounds on evaluation costs

Abstract

We develop a static complexity analysis for a higher-order functional language with structural list recursion. The complexity of an expression is a pair consisting of a cost and a potential. The former is defined to be the size of the expression's evaluation derivation in a standard big-step operational semantics. The latter is a measure of the "future" cost of using the value of that expression. A translation function tr maps target expressions to complexities. Our main result is the following Soundness Theorem: If t is a term in the target language, then the cost component of tr(t) is an upper bound on the cost of evaluating t. The proof of the Soundness Theorem is formalized in Coq, providing certified upper bounds on the cost of any expression in the target language.