Strong Call-by-Value and Multi Types

Beniamino Accattoli; Giulio Guerrieri; Maico Leberle

doi:10.1007/978-3-031-47963-2_13

Strong Call-by-Value and Multi Types

Beniamino Accattoli
, Giulio Guerrieri
, Maico Leberle

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

Abstract

This paper provides foundations for strong (that is, possibly under abstraction) call-by-value evaluation for the λ -calculus. Recently, Accattoli et al. proposed a form of call-by-value strong evaluation for the λ -calculus, the external strategy, and proved it reasonable for time. Here, we study the external strategy using a semantical tool, namely Ehrhard’s call-by-value multi types, a variant of intersection types. We show that the external strategy terminates exactly when a term is typable with so-called shrinking multi types, mimicking similar results for strong call-by-name. Additionally, the external strategy is normalizing in the untyped setting, that is, it reaches the normal form whenever it exists. We also consider the call-by-extended-value approach to strong evaluation shown reasonable for time by Biernacka et al. The two approaches turn out to not be equivalent: terms may be externally divergent but terminating for call-by-extended-value.

Original language	English
Title of host publication	Theoretical Aspects of Computing – ICTAC 2023 - 20th International Colloquium, Proceedings
Editors	Erika Ábrahám, Clemens Dubslaff, Silvia Lizeth Tarifa
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	196-215
Number of pages	20
ISBN (Print)	9783031479625
DOIs	https://doi.org/10.1007/978-3-031-47963-2_13
Publication status	Published - 1 Jan 2023
Event	20th International Colloquium on Theoretical Aspects of Computing, ICTAC 2023 - Lima, Peru Duration: 4 Dec 2023 → 8 Dec 2023

Publication series

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

Conference

Conference	20th International Colloquium on Theoretical Aspects of Computing, ICTAC 2023
Country/Territory	Peru
City	Lima
Period	4/12/23 → 8/12/23

Access to Document

10.1007/978-3-031-47963-2_13

Cite this

Accattoli, B., Guerrieri, G., & Leberle, M. (2023). Strong Call-by-Value and Multi Types. In E. Ábrahám, C. Dubslaff, & S. L. Tarifa (Eds.), Theoretical Aspects of Computing – ICTAC 2023 - 20th International Colloquium, Proceedings (pp. 196-215). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14446 LNCS). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-47963-2_13

Accattoli, Beniamino ; Guerrieri, Giulio ; Leberle, Maico. / Strong Call-by-Value and Multi Types. Theoretical Aspects of Computing – ICTAC 2023 - 20th International Colloquium, Proceedings. editor / Erika Ábrahám ; Clemens Dubslaff ; Silvia Lizeth Tarifa. Springer Science and Business Media Deutschland GmbH, 2023. pp. 196-215 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{fc1889de938c4c208a14cf36659d409c,

title = "Strong Call-by-Value and Multi Types",

abstract = "This paper provides foundations for strong (that is, possibly under abstraction) call-by-value evaluation for the λ -calculus. Recently, Accattoli et al. proposed a form of call-by-value strong evaluation for the λ -calculus, the external strategy, and proved it reasonable for time. Here, we study the external strategy using a semantical tool, namely Ehrhard{\textquoteright}s call-by-value multi types, a variant of intersection types. We show that the external strategy terminates exactly when a term is typable with so-called shrinking multi types, mimicking similar results for strong call-by-name. Additionally, the external strategy is normalizing in the untyped setting, that is, it reaches the normal form whenever it exists. We also consider the call-by-extended-value approach to strong evaluation shown reasonable for time by Biernacka et al. The two approaches turn out to not be equivalent: terms may be externally divergent but terminating for call-by-extended-value.",

author = "Beniamino Accattoli and Giulio Guerrieri and Maico Leberle",

note = "Publisher Copyright: {\textcopyright} 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.; 20th International Colloquium on Theoretical Aspects of Computing, ICTAC 2023 ; Conference date: 04-12-2023 Through 08-12-2023",

year = "2023",

month = jan,

day = "1",

doi = "10.1007/978-3-031-47963-2\_13",

language = "English",

isbn = "9783031479625",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "196--215",

editor = "Erika {\'A}brah{\'a}m and Clemens Dubslaff and Tarifa, \{Silvia Lizeth\}",

booktitle = "Theoretical Aspects of Computing – ICTAC 2023 - 20th International Colloquium, Proceedings",

}

Accattoli, B, Guerrieri, G & Leberle, M 2023, Strong Call-by-Value and Multi Types. in E Ábrahám, C Dubslaff & SL Tarifa (eds), Theoretical Aspects of Computing – ICTAC 2023 - 20th International Colloquium, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 14446 LNCS, Springer Science and Business Media Deutschland GmbH, pp. 196-215, 20th International Colloquium on Theoretical Aspects of Computing, ICTAC 2023, Lima, Peru, 4/12/23. https://doi.org/10.1007/978-3-031-47963-2_13

Strong Call-by-Value and Multi Types. / Accattoli, Beniamino; Guerrieri, Giulio; Leberle, Maico.
Theoretical Aspects of Computing – ICTAC 2023 - 20th International Colloquium, Proceedings. ed. / Erika Ábrahám; Clemens Dubslaff; Silvia Lizeth Tarifa. Springer Science and Business Media Deutschland GmbH, 2023. p. 196-215 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14446 LNCS).

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

TY - GEN

T1 - Strong Call-by-Value and Multi Types

AU - Accattoli, Beniamino

AU - Guerrieri, Giulio

AU - Leberle, Maico

PY - 2023/1/1

Y1 - 2023/1/1

N2 - This paper provides foundations for strong (that is, possibly under abstraction) call-by-value evaluation for the λ -calculus. Recently, Accattoli et al. proposed a form of call-by-value strong evaluation for the λ -calculus, the external strategy, and proved it reasonable for time. Here, we study the external strategy using a semantical tool, namely Ehrhard’s call-by-value multi types, a variant of intersection types. We show that the external strategy terminates exactly when a term is typable with so-called shrinking multi types, mimicking similar results for strong call-by-name. Additionally, the external strategy is normalizing in the untyped setting, that is, it reaches the normal form whenever it exists. We also consider the call-by-extended-value approach to strong evaluation shown reasonable for time by Biernacka et al. The two approaches turn out to not be equivalent: terms may be externally divergent but terminating for call-by-extended-value.

AB - This paper provides foundations for strong (that is, possibly under abstraction) call-by-value evaluation for the λ -calculus. Recently, Accattoli et al. proposed a form of call-by-value strong evaluation for the λ -calculus, the external strategy, and proved it reasonable for time. Here, we study the external strategy using a semantical tool, namely Ehrhard’s call-by-value multi types, a variant of intersection types. We show that the external strategy terminates exactly when a term is typable with so-called shrinking multi types, mimicking similar results for strong call-by-name. Additionally, the external strategy is normalizing in the untyped setting, that is, it reaches the normal form whenever it exists. We also consider the call-by-extended-value approach to strong evaluation shown reasonable for time by Biernacka et al. The two approaches turn out to not be equivalent: terms may be externally divergent but terminating for call-by-extended-value.

U2 - 10.1007/978-3-031-47963-2_13

DO - 10.1007/978-3-031-47963-2_13

M3 - Conference contribution

AN - SCOPUS:85178569693

SN - 9783031479625

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

SP - 196

EP - 215

BT - Theoretical Aspects of Computing – ICTAC 2023 - 20th International Colloquium, Proceedings

A2 - Ábrahám, Erika

A2 - Dubslaff, Clemens

A2 - Tarifa, Silvia Lizeth

PB - Springer Science and Business Media Deutschland GmbH

T2 - 20th International Colloquium on Theoretical Aspects of Computing, ICTAC 2023

Y2 - 4 December 2023 through 8 December 2023

ER -