Types of Fireballs

Beniamino Accattoli, Giulio Guerrieri

Research output: Chapter in Book/Report/Conference proceedingConference contribution

4 Citations (Scopus)

Abstract

The good properties of Plotkin’s call-by-value lambda-calculus crucially rely on the restriction to weak evaluation and closed terms. Open call-by-value is the more general setting where evaluation is weak but terms may be open. Such an extension is delicate and the literature contains a number of proposals. Recently, we provided operational and implementative studies of these proposals, showing that they are equivalent with respect to termination, and also at the level of time cost models. This paper explores the denotational semantics of open call-by-value, adapting de Carvalho’s analysis of call-by-name via multi types (aka non-idempotent intersection types). Our type system characterises normalisation and thus provides an adequate relational semantics. Moreover, type derivations carry quantitative information about the cost of evaluation: their size bounds the number of evaluation steps and the size of the normal form, and we also characterise derivations giving exact bounds. The study crucially relies on a new, refined presentation of the fireball calculus, the simplest proposal for open call-by-value, that is more apt to denotational investigations.

Original languageEnglish
Title of host publicationProgramming Languages and Systems - 16th Asian Symposium, APLAS 2018, Proceedings
EditorsSukyoung Ryu
PublisherSpringer Verlag
Pages45-66
Number of pages22
ISBN (Print)9783030027674
DOIs
Publication statusE-pub ahead of print - 22 Oct 2018
Event16th Asian Symposium on Programming Languages and Systems, APLAS 2018 - Wellington, New Zealand
Duration: 2 Dec 20186 Dec 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11275 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference16th Asian Symposium on Programming Languages and Systems, APLAS 2018
CountryNew Zealand
CityWellington
Period2/12/186/12/18

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Accattoli, B., & Guerrieri, G. (2018). Types of Fireballs. In S. Ryu (Ed.), Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Proceedings (pp. 45-66). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11275 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-030-02768-1_3

Types of Fireballs. / Accattoli, Beniamino; Guerrieri, Giulio.

Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Proceedings. ed. / Sukyoung Ryu. Springer Verlag, 2018. p. 45-66 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11275 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Accattoli, B & Guerrieri, G 2018, Types of Fireballs. in S Ryu (ed.), Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11275 LNCS, Springer Verlag, pp. 45-66, 16th Asian Symposium on Programming Languages and Systems, APLAS 2018, Wellington, New Zealand, 2/12/18. https://doi.org/10.1007/978-3-030-02768-1_3
Accattoli B, Guerrieri G. Types of Fireballs. In Ryu S, editor, Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Proceedings. Springer Verlag. 2018. p. 45-66. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-02768-1_3
Accattoli, Beniamino ; Guerrieri, Giulio. / Types of Fireballs. Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Proceedings. editor / Sukyoung Ryu. Springer Verlag, 2018. pp. 45-66 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{afe2fb5fb8a84dc7ab47b8e2a297da9c,
title = "Types of Fireballs",
abstract = "The good properties of Plotkin’s call-by-value lambda-calculus crucially rely on the restriction to weak evaluation and closed terms. Open call-by-value is the more general setting where evaluation is weak but terms may be open. Such an extension is delicate and the literature contains a number of proposals. Recently, we provided operational and implementative studies of these proposals, showing that they are equivalent with respect to termination, and also at the level of time cost models. This paper explores the denotational semantics of open call-by-value, adapting de Carvalho’s analysis of call-by-name via multi types (aka non-idempotent intersection types). Our type system characterises normalisation and thus provides an adequate relational semantics. Moreover, type derivations carry quantitative information about the cost of evaluation: their size bounds the number of evaluation steps and the size of the normal form, and we also characterise derivations giving exact bounds. The study crucially relies on a new, refined presentation of the fireball calculus, the simplest proposal for open call-by-value, that is more apt to denotational investigations.",
author = "Beniamino Accattoli and Giulio Guerrieri",
year = "2018",
month = "10",
day = "22",
doi = "10.1007/978-3-030-02768-1_3",
language = "English",
isbn = "9783030027674",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "45--66",
editor = "Sukyoung Ryu",
booktitle = "Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Proceedings",

}

TY - GEN

T1 - Types of Fireballs

AU - Accattoli, Beniamino

AU - Guerrieri, Giulio

PY - 2018/10/22

Y1 - 2018/10/22

N2 - The good properties of Plotkin’s call-by-value lambda-calculus crucially rely on the restriction to weak evaluation and closed terms. Open call-by-value is the more general setting where evaluation is weak but terms may be open. Such an extension is delicate and the literature contains a number of proposals. Recently, we provided operational and implementative studies of these proposals, showing that they are equivalent with respect to termination, and also at the level of time cost models. This paper explores the denotational semantics of open call-by-value, adapting de Carvalho’s analysis of call-by-name via multi types (aka non-idempotent intersection types). Our type system characterises normalisation and thus provides an adequate relational semantics. Moreover, type derivations carry quantitative information about the cost of evaluation: their size bounds the number of evaluation steps and the size of the normal form, and we also characterise derivations giving exact bounds. The study crucially relies on a new, refined presentation of the fireball calculus, the simplest proposal for open call-by-value, that is more apt to denotational investigations.

AB - The good properties of Plotkin’s call-by-value lambda-calculus crucially rely on the restriction to weak evaluation and closed terms. Open call-by-value is the more general setting where evaluation is weak but terms may be open. Such an extension is delicate and the literature contains a number of proposals. Recently, we provided operational and implementative studies of these proposals, showing that they are equivalent with respect to termination, and also at the level of time cost models. This paper explores the denotational semantics of open call-by-value, adapting de Carvalho’s analysis of call-by-name via multi types (aka non-idempotent intersection types). Our type system characterises normalisation and thus provides an adequate relational semantics. Moreover, type derivations carry quantitative information about the cost of evaluation: their size bounds the number of evaluation steps and the size of the normal form, and we also characterise derivations giving exact bounds. The study crucially relies on a new, refined presentation of the fireball calculus, the simplest proposal for open call-by-value, that is more apt to denotational investigations.

UR - http://www.scopus.com/inward/record.url?scp=85057828397&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-02768-1_3

DO - 10.1007/978-3-030-02768-1_3

M3 - Conference contribution

SN - 9783030027674

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 45

EP - 66

BT - Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Proceedings

A2 - Ryu, Sukyoung

PB - Springer Verlag

ER -