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