Type-Based Allocation Analysis for Co-recursion in Lazy Functional Languages

• Type: Article in International Conference Proceedings Book
• Date: 2015

Authors

Pedro Vasconcelos (Author) FCUP; Steffen Jost (Author) Other; Mario Florido (Author) FCUP; Kevin Hammond (Author) Other

Conference proceedings International

Title: PROGRAMMING LANGUAGES AND SYSTEMS

Pages: 787-811

24th European Conference on Programming (ESOP) held as Part of the 18th European Joint Conferences on Theory and Practice of Software (ETAPS)

London, ENGLAND, APR 11-18, 2015

Indexing

ISI Web of Knowledge - 7 Citations

Scopus - 8 Citations

Scientific classification

FOS: Natural sciences > Computer and information sciences

Other information

Authenticus ID: P-00A-AWP

DOI: 10.1007/978-3-662-46669-8_32

Abstract (EN): 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.

Language: English

Type (Professor's evaluation): Scientific

No. of pages: 25