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

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

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

5 Citations (Scopus)
2 Downloads (Pure)

Abstract

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
PublisherSpringer-Verlag
Pages787-811
Number of pages25
Volume9032
ISBN (Electronic)978-3-662-46669-8
ISBN (Print)978-3-662-46668-1
DOIs
Publication statusPublished - 2015
Event24th European Symposium on Programming, ESOP 2015 - Queen Mary, University of London, London, United Kingdom
Duration: 14 Apr 201516 Apr 2015
http://conf.researchr.org/home/esop-2015

Publication series

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

Conference

Conference24th European Symposium on Programming, ESOP 2015
Country/TerritoryUnited Kingdom
CityLondon
Period14/04/1516/04/15
Internet address

Fingerprint

Dive into the research topics of 'Type-based allocation analysis for co-recursion in lazy functional languages'. Together they form a unique fingerprint.

Cite this