Projects per year
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.
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 | |
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 |
Fingerprint
Dive into the research topics of 'Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic'. Together they form a unique fingerprint.Projects
- 1 Active
-
Typed Lambda-Calculi with Sharing and Unsharing
Engineering and Physical Sciences Research Council
1/01/19 → 30/07/22
Project: Research council