Skip to content

Research at St Andrews

Type-based allocation analysis for co-recursion in lazy functional languages

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


Pedro Baltazar Vasconcelos, Steffen Jost, Mario Florido, Kevin Hammond

School/Research organisations


This paper presents a novel type-and-effect analysis for pre-dicting upper-bounds on memory allocation costs for co-recursive def-initions in a simple lazily-evaluated functional language. We show thesoundness of this system against an instrumented variant of Launch-bury’s semantics for lazy evaluation which serves as a formal cost model.Our soundness proof requires an intermediate semantics employing indi-rections. Our proof of correspondence between these semantics that weprovide is thus a crucial part of this work.The analysis has been implemented as an automatic inference system.We demonstrate its effectiveness using several example programs thatpreviously could not be automatically analysed.


Original languageEnglish
Title of host publicationProgramming Languages and Systems
Subtitle of host publication24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings
EditorsJan Vitek
Number of pages25
ISBN (Electronic)978-3-662-46669-8
ISBN (Print)978-3-662-46668-1
Publication statusPublished - 2015
Event24th European Symposium on Programming, ESOP 2015 - Queen Mary, University of London, London, United Kingdom
Duration: 14 Apr 201516 Apr 2015

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Conference24th European Symposium on Programming, ESOP 2015
CountryUnited Kingdom
Internet address

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

View graph of relations

ID: 159586916