DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2022.4

Useful Open Call-By-Need

Authors: Beniamino Accattoli and Maico Leberle

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

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.

Cite as

Beniamino Accattoli and Maico Leberle. Useful Open Call-By-Need. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 4:1-4:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{accattoli_et_al:LIPIcs.CSL.2022.4,
  author =	{Accattoli, Beniamino and Leberle, Maico},
  title =	{{Useful Open Call-By-Need}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{4:1--4:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.4},
  URN =		{urn:nbn:de:0030-drops-157242},
  doi =		{10.4230/LIPIcs.CSL.2022.4},
  annote =	{Keywords: lambda calculus, call-by-need, operational semantics, sharing, cost models}
}

Search Results

Documents authored by Leberle, Maico

Useful Open Call-By-Need

Abstract

Cite as

Thanks for your feedback!

Could not send message