TY - GEN
T1 - Strong Call-by-Value and Multi Types
AU - Accattoli, Beniamino
AU - Guerrieri, Giulio
AU - Leberle, Maico
N1 - Publisher Copyright:
© 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.
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.
UR - https://www.scopus.com/pages/publications/85178569693
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 -