Useful Open Call-By-Need

Beniamino Accattoli, Maico Leberle

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

This paper studies useful sharing, which is a sophisticated optimization for λ-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.

Original languageEnglish
Title of host publication30th EACSL Annual Conference on Computer Science Logic, CSL 2022
EditorsFlorin Manea, Alex Simpson
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (Electronic)9783959772181
DOIs
Publication statusPublished - 1 Feb 2022
Event30th EACSL Annual Conference on Computer Science Logic, CSL 2022 - Virtual, Gottingen, Germany
Duration: 14 Feb 202219 Feb 2022

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume216
ISSN (Print)1868-8969

Conference

Conference30th EACSL Annual Conference on Computer Science Logic, CSL 2022
Country/TerritoryGermany
CityVirtual, Gottingen
Period14/02/2219/02/22

Keywords

  • Call-by-need
  • Cost models
  • Lambda calculus
  • Operational semantics
  • Sharing

Fingerprint

Dive into the research topics of 'Useful Open Call-By-Need'. Together they form a unique fingerprint.

Cite this