Paper Info
Title
Type-Based Allocation Analysis for Co-recursion in Lazy Functional Languages.
Abstract
This paper presents a novel type-and-effect analysis for predicting upper-bounds on memory allocation costs for co-recursive definitions in a simple lazily-evaluated functional language. We show the soundness 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 indirections. Our proof of correspondence between these semantics that we provide 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 that previously could not be automatically analysed.
Year
DOI
Venue
2015
10.1007/978-3-662-46669-8_32
Lecture Notes in Computer Science
Field
DocType
Volume
Programming language,Functional programming,Computer science,Lazy evaluation,Type rule,Theoretical computer science,Memory management,Soundness,Proof obligation,Semantics,Recursion
Conference
9032
ISSN
Citations 
PageRank 
0302-9743
6
0.42
References 
Authors
17
4
Name
Order
Citations
PageRank
Pedro B. Vasconcelos181.12
Steffen Jost224712.36
Mário Florido312214.44
Kevin Hammond437323.36