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

This paper studies the problem of statically determining upper bounds on the resource consumption of first-order functional programs. A previous work approached the problem with an automatic type-based amortized analysis for polynomial resource bounds. The analysis is parametric in the resource and can be instantiated to heap space, stack space, or clock cycles. Experiments with a prototype implementation have shown that programs are analyzed efficiently and that the computed bounds exactly match the measured worst-case resource behavior for many functions. This paper describes the inference algorithm that is used in the implementation of the system. It can deal with resource-polymorphic recursion which is required in the type derivation of many functions. The computation of the bounds is fully automatic if a maximal degree of the polynomials is given. The soundness of the inference is proved with respect to a novel operational semantics for partial evaluations to show that the inferre...

• Type: Conference
• Year: 2010
• Where: APLAS
• Authors: Jan Hoffmann 0002, Martin Hofmann
• Keywords: APLAS 2010, First-order Functional Programs, Programming Languages, Resource, Upper Bounds