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

Claudia Faggian, Giulio Guerrieri

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish
Title of host publication24th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2021
PublisherSpringer Verlag
Publication statusE-pub ahead of print - 2021
Event24th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2021 -
Duration: 29 Mar 2021 → …
https://etaps.org/2021/fossacs

Publication series

NameLecture Notes in Computer Science

Conference

Conference24th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2021
Period29/03/21 → …
Internet address

Cite this