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

Author(s)

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

School/Research organisations

Abstract

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.
Close

Details

Original languageEnglish
Title of host publicationICFP '12 Proceedings of the 17th ACM SIGPLAN international conference on Functional programming
Place of PublicationNew York
PublisherACM
Pages165-176
Number of pages12
ISBN (Print) 978-1-4503-1054-3
DOIs
StatePublished - 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

Related by author

  1. Automatically deriving cost models for structured parallel processes using hylomorphisms

    Castro, D., Hammond, K., Sarkar, S. & Alguwaifli, Y. Feb 2018 In : Future Generation Computer Systems. 79, Part 2, p. 653-668

    Research output: Contribution to journalArticle

  2. The Missing Link! A new skeleton for evolutionary multi-agent systems in Erlang

    Stypka, J., Turek, W., Byrski, A., Kisiel-Dorohinicki, M., Barwell, A. D., Brown, C. M., Hammond, K. & Janjic, V. Feb 2018 In : International Journal of Parallel Programming. 46, 1, p. 4-22 19 p.

    Research output: Contribution to journalArticle

  3. Proof-relevant Horn clauses for dependent type inference and term synthesis

    Farka, F., Komendantskya, E. & Hammond, K. 2018 In : Theory and Practice of Logic Programming. 18, 3-4, p. 484-501

    Research output: Contribution to journalArticle

  4. Type-based cost analysis for lazy functional languages

    Jost, S., Vasconcelos, P., Florido, M. & Hammond, K. Jun 2017 In : Journal of Automated Reasoning. 59, 1, p. 87-120 34 p.

    Research output: Contribution to journalArticle

ID: 21561945