Projects per year
Abstract
A cornerstone of the theory of lambda-calculus is that intersection types characterise termination properties. They are a flexible tool that can be adapted to various notions of termination, and that also induces adequate denotational models. Since the seminal work of de Carvalho in 2007, it is known that multi types (i.e. non-idempotent intersection types) refine intersection types with quantitative information and a strong connection to linear logic. Typically, type derivations provide bounds for evaluation lengths, and minimal type derivations provide exact bounds. De Carvalho studied call-by-name evaluation, and Kesner used his system to show the termination equivalence of call-by-need and call-by-name. De Carvalho’s system, however, cannot provide exact bounds on call-by-need evaluation lengths. In this paper we develop a new multi type system for call-by-need. Our system produces exact bounds and induces a denotational model of call-by-need, providing the first tight quantitative semantics of call-by-need.
Original language | English |
---|---|
Title of host publication | Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings |
Editors | Luís Caires |
Publisher | Springer Verlag |
Pages | 410-439 |
Number of pages | 30 |
ISBN (Print) | 9783030171834 |
DOIs | |
Publication status | Published - 29 Apr 2019 |
Event | 28th European Symposium on Programming, ESOP 2019 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019 - Prague, Czech Republic Duration: 6 Apr 2019 → 11 Apr 2019 |
Publication series
Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 11423 |
Conference
Conference | 28th European Symposium on Programming, ESOP 2019 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019 |
---|---|
Country/Territory | Czech Republic |
City | Prague |
Period | 6/04/19 → 11/04/19 |
Funding
Acknowledgements. This work has been partially funded by the ANR JCJC grant COCA HOLA (ANR-16-CE40-004-01) and by the EPSRC grant EP/R029121/1 “Typed Lambda-Calculi with Sharing and Unsharing”.
ASJC Scopus subject areas
- Theoretical Computer Science
- General Computer Science
Fingerprint
Dive into the research topics of 'Types by Need'. Together they form a unique fingerprint.Projects
- 1 Finished
-
Typed Lambda-Calculi with Sharing and Unsharing
Heijltjes, W. (PI)
Engineering and Physical Sciences Research Council
1/01/19 → 30/07/22
Project: Research council