Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic (long version)
Logic in Computer Science
2021-01-22 v1
Abstract
In each variant of the lambda-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 lambda-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.
Keywords
Cite
@article{arxiv.2101.08364,
title = {Factorization in Call-by-Name and Call-by-Value Calculi via Linear Logic (long version)},
author = {Claudia Faggian and Giulio Guerrieri},
journal= {arXiv preprint arXiv:2101.08364},
year = {2021}
}