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

Claudia Faggian; Giulio Guerrieri

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

Department of Computer Science

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

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
Publisher	Springer Verlag
Publication status	E-pub ahead of print - 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

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

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 → 31/12/21
Project: Research council

Cite this

Faggian, C & Guerrieri, G 2021, Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic. in 24th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2021. Lecture Notes in Computer Science, Springer Verlag, 24th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2021, 29/03/21.

@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",

language = "English",

series = "Lecture Notes in Computer Science",

publisher = "Springer Verlag",

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

Y1 - 2021

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.

M3 - Conference contribution

T3 - Lecture Notes in Computer Science

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

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

Typed Lambda-Calculi with Sharing and Unsharing

Cite this