Title

A static cost analysis for a higher-order language

Document Type

Article

Publication Date

2013

Journal or Book Title

Proceedings of the 7th workshop on Programming languages meets program verification

First Page

25

Last Page

34

Editor

Matthew Might, David Van Horn

Publisher

ACM Press

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 ||.|| 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 ||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.

Comments

The code provided here is the code that was associated to this paper when it was published. Please see the Computer Science "Code and data" section for the most current version of the code provided here.

static_cost.tgz (16 kB)
Coq development of Soundness Theorem.