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

Claudia Faggian, Giulio Guerrieri

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

4 Citations (SciVal)
24 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 languageEnglish
Title of host publicationFoundations 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
EditorsStefan Kiefer, Christine Tasson
PublisherSpringer Verlag
Pages205-225
Number of pages21
ISBN (Print)9783030719944
DOIs
Publication statusPublished - 23 Mar 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 (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12650
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

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

Bibliographical 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:
© The Author(s) 2021.

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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.

Cite this