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 or section in a book/report/conference proceeding › Chapter in a published conference proceeding

4 Citations (SciVal)

8 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	Foundations of Software Science and Computation Structures - 24th International Conference, FOSSACS 2021 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Proceedings
Editors	Stefan Kiefer, Christine Tasson
Publisher	Springer Verlag
Pages	205-225
Number of pages	21
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 (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12650
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

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

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

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

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.), Foundations of Software Science and Computation Structures - 24th International Conference, FOSSACS 2021 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Proceedings (pp. 205-225). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); 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.

Foundations of Software Science and Computation Structures - 24th International Conference, FOSSACS 2021 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Proceedings. ed. / Stefan Kiefer; Christine Tasson. Springer Verlag, 2021. p. 205-225 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12650).

Research output: Chapter or section in a book/report/conference proceeding › Chapter in a published conference proceeding

Faggian, C & Guerrieri, G 2021, Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic. in S Kiefer & C Tasson (eds), Foundations of Software Science and Computation Structures - 24th International Conference, FOSSACS 2021 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 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

Faggian C, Guerrieri G. Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic. In Kiefer S, Tasson C, editors, Foundations of Software Science and Computation Structures - 24th International Conference, FOSSACS 2021 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Proceedings. Springer Verlag. 2021. p. 205-225. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-71995-1_11

Faggian, Claudia ; Guerrieri, Giulio. / Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic. Foundations of Software Science and Computation Structures - 24th International Conference, FOSSACS 2021 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Proceedings. editor / Stefan Kiefer ; Christine Tasson. Springer Verlag, 2021. pp. 205-225 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

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

note = "Funding Information: Acknowledgments. The authors thank Beniamino Accattoli for insightful comments and discussions. This work was partially supported by EPSRC Project EP/R029121/1 Typed Lambda-Calculi with Sharing and Unsharing. Publisher Copyright: {\textcopyright} The Author(s) 2021.; 24th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2021 ; Conference date: 29-03-2021",

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 (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "205--225",

editor = "Stefan Kiefer and Christine Tasson",

booktitle = "Foundations of Software Science and Computation Structures - 24th International Conference, FOSSACS 2021 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Proceedings",

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

N1 - Funding Information: Acknowledgments. The authors thank Beniamino Accattoli for insightful comments and discussions. This work was partially supported by EPSRC Project EP/R029121/1 Typed Lambda-Calculi with Sharing and Unsharing. Publisher Copyright: © The Author(s) 2021.

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.

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

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

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

M3 - Chapter in a published conference proceeding

SN - 9783030719944

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

SP - 205

EP - 225

BT - Foundations of Software Science and Computation Structures - 24th International Conference, FOSSACS 2021 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Proceedings

A2 - Kiefer, Stefan

A2 - Tasson, Christine

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

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Typed Lambda-Calculi with Sharing and Unsharing

Cite this

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

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Projects

Typed Lambda-Calculi with Sharing and Unsharing

Cite this