×

Amortized resource analysis with polynomial potential. A static inference of polynomial bounds for functional programs. (English) Zbl 1260.68074

Gordon, Andrew D. (ed.), Programming languages and systems. 19th European symposium on programming, ESOP 2010, held as part of the joint European conferences on theory and practice of software, ETAPS 2010, Paphos, Cyprus, March 20–28, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-11956-9/pbk). Lecture Notes in Computer Science 6012, 287-306 (2010).
Summary: In 2003, Hofmann and Jost introduced a type system that uses a potential-based amortized analysis to infer bounds on the resource consumption of (first-order) functional programs. This analysis has been successfully applied to many standard algorithms but is limited to bounds that are linear in the size of the input.
Here we extend this system to polynomial resource bounds. An automatic amortized analysis is used to infer these bounds for functional programs without further annotations if a maximal degree for the bounding polynomials is given. The analysis is generic in the resource and can obtain good bounds on heap-space, stack-space and time usage.
For the entire collection see [Zbl 1182.68003].

MSC:

68N18 Functional programming and lambda calculus
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Software:

SPEED
PDFBibTeX XMLCite
Full Text: DOI