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

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

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

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 proceeding › Conference contribution

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 language	English
Title of host publication	Programming Languages and Systems
Subtitle of host publication	24th 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
Editors	Jan Vitek
Publisher	Springer-Verlag
Pages	787-811
Number of pages	25
Volume	9032
ISBN (Electronic)	978-3-662-46669-8
ISBN (Print)	978-3-662-46668-1
DOIs	https://doi.org/10.1007/978-3-662-46669-8_32
Publication status	Published - 2015
Event	24th European Symposium on Programming, ESOP 2015 - Queen Mary, University of London, London, United Kingdom Duration: 14 Apr 2015 → 16 Apr 2015 http://conf.researchr.org/home/esop-2015

Publication series

Name	Lecture Notes in Computer Science
ISSN (Print)	0302-9743

Conference

Conference	24th European Symposium on Programming, ESOP 2015
Country/Territory	United Kingdom
City	London
Period	14/04/15 → 16/04/15
Internet address	http://conf.researchr.org/home/esop-2015

Access to Document

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

LazyCoRec2
© Springer-Verlag Berlin Heidelberg 2015. The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-662-46669-8_32
Accepted author manuscript, 620 KB

ParaPhrase FP7-ICT-2011-7: EU FP7 'ParaPhrase'
Hammond, K. (PI)
European Commission
1/10/11 → 31/03/15
Project: Standard
EP/F030657/1 Adaptive Hardware Systems: Copy of Adaptive Hardware Systems with Novel Algorithmic Design and Guaranteed Resource Bounds
Hammond, K. (PI)
EPSRC
1/09/08 → 31/08/11
Project: Standard

Cite this

Vasconcelos, P. B., Jost, S., Florido, M., & Hammond, K. (2015). Type-based allocation analysis for co-recursion in lazy functional languages. In J. Vitek (Ed.), Programming Languages and Systems: 24th 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 (Vol. 9032, pp. 787-811). (Lecture Notes in Computer Science). Springer-Verlag. https://doi.org/10.1007/978-3-662-46669-8_32

Vasconcelos, Pedro Baltazar ; Jost, Steffen ; Florido, Mario et al. / Type-based allocation analysis for co-recursion in lazy functional languages. Programming Languages and Systems: 24th 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. editor / Jan Vitek. Vol. 9032 Springer-Verlag, 2015. pp. 787-811 (Lecture Notes in Computer Science).

@inproceedings{3656a19822f948559b2d158a607430ae,

title = "Type-based allocation analysis for co-recursion in lazy functional languages",

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{\textquoteright}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.",

author = "Vasconcelos, {Pedro Baltazar} and Steffen Jost and Mario Florido and Kevin Hammond",

year = "2015",

doi = "10.1007/978-3-662-46669-8_32",

language = "English",

isbn = "978-3-662-46668-1",

volume = "9032",

series = "Lecture Notes in Computer Science",

publisher = "Springer-Verlag",

pages = "787--811",

editor = "Jan Vitek",

booktitle = "Programming Languages and Systems",

address = "Germany",

note = "24th European Symposium on Programming, ESOP 2015 ; Conference date: 14-04-2015 Through 16-04-2015",

url = "http://conf.researchr.org/home/esop-2015",

}

Vasconcelos, PB, Jost, S, Florido, M & Hammond, K 2015, Type-based allocation analysis for co-recursion in lazy functional languages. in J Vitek (ed.), Programming Languages and Systems: 24th 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. vol. 9032, Lecture Notes in Computer Science, Springer-Verlag, pp. 787-811, 24th European Symposium on Programming, ESOP 2015, London, United Kingdom, 14/04/15. https://doi.org/10.1007/978-3-662-46669-8_32

Type-based allocation analysis for co-recursion in lazy functional languages. / Vasconcelos, Pedro Baltazar; Jost, Steffen; Florido, Mario et al.
Programming Languages and Systems: 24th 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. ed. / Jan Vitek. Vol. 9032 Springer-Verlag, 2015. p. 787-811 (Lecture Notes in Computer Science).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

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

AU - Vasconcelos, Pedro Baltazar

AU - Jost, Steffen

AU - Florido, Mario

AU - Hammond, Kevin

PY - 2015

Y1 - 2015

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

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

U2 - 10.1007/978-3-662-46669-8_32

DO - 10.1007/978-3-662-46669-8_32

M3 - Conference contribution

SN - 978-3-662-46668-1

VL - 9032

T3 - Lecture Notes in Computer Science

SP - 787

EP - 811

BT - Programming Languages and Systems

A2 - Vitek, Jan

PB - Springer-Verlag

T2 - 24th European Symposium on Programming, ESOP 2015

Y2 - 14 April 2015 through 16 April 2015

ER -

Vasconcelos PB, Jost S, Florido M, Hammond K. Type-based allocation analysis for co-recursion in lazy functional languages. In Vitek J, editor, Programming Languages and Systems: 24th 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. Vol. 9032. Springer-Verlag. 2015. p. 787-811. (Lecture Notes in Computer Science). doi: 10.1007/978-3-662-46669-8_32

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

Abstract

Publication series

Conference

Access to Document

Fingerprint

Projects

ParaPhrase FP7-ICT-2011-7: EU FP7 'ParaPhrase'

EP/F030657/1 Adaptive Hardware Systems: Copy of Adaptive Hardware Systems with Novel Algorithmic Design and Guaranteed Resource Bounds

Cite this