Sciweavers

Share
APLAS
2010
ACM

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

8 years 3 months ago
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...
Jan Hoffmann 0002, Martin Hofmann
Added 05 Dec 2010
Updated 05 Dec 2010
Type Conference
Year 2010
Where APLAS
Authors Jan Hoffmann 0002, Martin Hofmann
Comments (0)
books