Skip to content

Research at St Andrews

Automatic Amortised Analysis of Dynamic Memory Allocation for Lazy Functional Programs

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Hugo Miguel Simoes, Pedro Baltazar Vasconcelos, Mario Florido, Steffen Jost, Kevin Hammond

School/Research organisations


This paper describes the first successful attempt, of which we are
aware, to define an automatic, type-based static analysis of resource
bounds for lazy functional programs. Our analysis uses the automatic
amortisation approach developed by Jost and Hofmann, which was
previously restricted to eager evaluation. In this paper, we extend
this work to a lazy setting by capturing the costs of unevaluated
expressions in type annotations and by amortising the payment of these
costs using a notion of lazy potential. We present our analysis as a
proof system for predicting heap allocations of a minimal functional
language (including higher-order functions and recursive data types)
and define a formal cost model based on Launchbury's natural semantics
for lazy evaluation. We prove the soundness of our analysis with
respect to the cost model. Our approach is illustrated by a number of
representative and non-trivial examples that have been analyed using a
prototype implementation of our analysis.


Original languageEnglish
Title of host publicationICFP '12 Proceedings of the 17th ACM SIGPLAN international conference on Functional programming
Place of PublicationNew York
Number of pages12
ISBN (Print) 978-1-4503-1054-3
Publication statusPublished - 2012

    Research areas

  • Functional Programming, Lazy evaluation, Cost Modelling, Operational Semantics, TYPE SYSTEMS

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

ID: 21561945