Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic

Claudia Faggian; Giulio Guerrieri

doi:10.1007/978-3-030-71995-1_11

Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic

Claudia Faggian, Giulio Guerrieri

Department of Computer Science

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

6 Downloads (Pure)

Abstract

In each variant of the λ-calculus, factorization and normalization are two key properties that show how results are computed.
Instead of proving factorization/normalization for the call-by-name (CbN) and call-by-value (CbV) variants separately, we prove them only once, for the bang calculus (an extension of the λ-calculus inspired by linear logic and subsuming CbN and CbV), and then we transfer the result via translations, obtaining factorization/normalization for CbN and CbV.
The approach is robust: it still holds when extending the calculi with operators and extra rules to model some additional computational features.

Original language	English
Title of host publication	24th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2021
Editors	S. Kiefer, C. Tasson
Publisher	Springer Verlag
Pages	205-225
ISBN (Print)	9783030719944
DOIs	https://doi.org/10.1007/978-3-030-71995-1_11
Publication status	Published - 23 Mar 2021
Event	24th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2021 - Duration: 29 Mar 2021 → … https://etaps.org/2021/fossacs

Publication series

Name	Lecture Notes in Computer Science
Volume	12650

Conference

Conference	24th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2021
Period	29/03/21 → …
Internet address	https://etaps.org/2021/fossacs

Access to Document

10.1007/978-3-030-71995-1_11

Factorization_in_Call-by-Name_and_Call-by-Value_Calculi_via_Linear_LogicProof, 463 KB

1 Active

Typed Lambda-Calculi with Sharing and Unsharing
Heijltjes, W.
Engineering and Physical Sciences Research Council
1/01/19 → 30/07/22
Project: Research council

Cite this

Faggian, C., & Guerrieri, G. (2021). Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic. In S. Kiefer, & C. Tasson (Eds.), 24th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2021 (pp. 205-225). (Lecture Notes in Computer Science; Vol. 12650). Springer Verlag. https://doi.org/10.1007/978-3-030-71995-1_11

Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic. / Faggian, Claudia; Guerrieri, Giulio.

24th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2021. ed. / S. Kiefer; C. Tasson. Springer Verlag, 2021. p. 205-225 (Lecture Notes in Computer Science; Vol. 12650).

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

Faggian, C & Guerrieri, G 2021, Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic. in S Kiefer & C Tasson (eds), 24th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2021. Lecture Notes in Computer Science, vol. 12650, Springer Verlag, pp. 205-225, 24th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2021, 29/03/21. https://doi.org/10.1007/978-3-030-71995-1_11

@inproceedings{f170a4a817564bd190e3a6940d8889b1,

title = "Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic",

abstract = "In each variant of the λ-calculus, factorization and normalization are two key properties that show how results are computed.Instead of proving factorization/normalization for the call-by-name (CbN) and call-by-value (CbV) variants separately, we prove them only once, for the bang calculus (an extension of the λ-calculus inspired by linear logic and subsuming CbN and CbV), and then we transfer the result via translations, obtaining factorization/normalization for CbN and CbV.The approach is robust: it still holds when extending the calculi with operators and extra rules to model some additional computational features.",

author = "Claudia Faggian and Giulio Guerrieri",

year = "2021",

month = mar,

day = "23",

doi = "10.1007/978-3-030-71995-1_11",

language = "English",

isbn = "9783030719944",

series = "Lecture Notes in Computer Science",

publisher = "Springer Verlag",

pages = "205--225",

editor = "S. Kiefer and C. Tasson",

booktitle = "24th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2021",

note = "24th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2021 ; Conference date: 29-03-2021",

url = "https://etaps.org/2021/fossacs",

}

TY - GEN

T1 - Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic

AU - Faggian, Claudia

AU - Guerrieri, Giulio

PY - 2021/3/23

Y1 - 2021/3/23

N2 - In each variant of the λ-calculus, factorization and normalization are two key properties that show how results are computed.Instead of proving factorization/normalization for the call-by-name (CbN) and call-by-value (CbV) variants separately, we prove them only once, for the bang calculus (an extension of the λ-calculus inspired by linear logic and subsuming CbN and CbV), and then we transfer the result via translations, obtaining factorization/normalization for CbN and CbV.The approach is robust: it still holds when extending the calculi with operators and extra rules to model some additional computational features.

AB - In each variant of the λ-calculus, factorization and normalization are two key properties that show how results are computed.Instead of proving factorization/normalization for the call-by-name (CbN) and call-by-value (CbV) variants separately, we prove them only once, for the bang calculus (an extension of the λ-calculus inspired by linear logic and subsuming CbN and CbV), and then we transfer the result via translations, obtaining factorization/normalization for CbN and CbV.The approach is robust: it still holds when extending the calculi with operators and extra rules to model some additional computational features.

U2 - 10.1007/978-3-030-71995-1_11

DO - 10.1007/978-3-030-71995-1_11

M3 - Conference contribution

SN - 9783030719944

T3 - Lecture Notes in Computer Science

SP - 205

EP - 225

BT - 24th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2021

A2 - Kiefer, S.

A2 - Tasson, C.

PB - Springer Verlag

T2 - 24th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2021

Y2 - 29 March 2021

ER -

Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic

Abstract

Publication series

Conference

Access to Document

Fingerprint

Projects

Typed Lambda-Calculi with Sharing and Unsharing

Cite this