Useful Open Call-by-Need
Logic in Computer Science
2021-10-29 v2 Programming Languages
Abstract
This paper studies useful sharing, which is a sophisticated optimization for lambda-calculi, in the context of call-by-need evaluation in presence of open terms. Useful sharing turns out to be harder in call-by-need than in call-by-name or call-by-value, because call-by-need evaluates inside environments, making it harder to specify when a substitution step is useful. We isolate the key involved concepts and prove the correctness and the completeness of useful sharing in this setting.
Keywords
Cite
@article{arxiv.2107.06591,
title = {Useful Open Call-by-Need},
author = {Beniamino Accattoli and Maico Leberle},
journal= {arXiv preprint arXiv:2107.06591},
year = {2021}
}
Comments
This is the version with proofs of the paper with the same title and authors in the proceedings of CSL 2022