Jan Hoffmann: Amortized Resource Analysis with Polymorphic Recursion and Partial Big-Step Operational Semantics

Recently we developed an automatic amortized analysis to compute polynomial resource bounds for first-order functional programs at compile time. Its basis is a type system that augments types with resource annotations.

For many functions it is necessary to allow recursive calls with a resource annotation different from the one that is being justified. A main challenge in the type inference is the need to deal with this resource-polymorphic recursion.

In my talk I will present the inference algorithm that is implemented in the programming language Resource Aware ML. Although it is not complete, it infers resource-polymorphic types for many functions we tested. Our experiments show that the algorithm is efficient and that the computed bounds exactly match the measured worst-case resource behavior for many functions.

The soundness of the inference is proved with respect to a novel operational semantics for partial evaluations to show that the inferred bounds hold for terminating as well as non-terminating computations. A corollary is that run-time bounds also establish the termination of programs.

The talk is based on a joint work with Martin Hofmann that will appear at APLAS 2010.