Useful Open Call-By-Need

DOI10.4230/LIPICS.CSL.2022.4MaRDI QIDQ6124931zbMATH OpenOpenAlexFDO

Authors Beniamino Accattoli, Maico Leberle

Publication date 10 April 2024

Full work available at URL https://arxiv.org/abs/2107.06591

zbMATH Keywords

lambda calculussharingoperational semanticscall-by-needcost models

Mathematics Subject Classification ID

Logic in computer science (03B70)

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.

Recommendations

• The call-by-need lambda calculus
• Weak optimality, and the meaning of sharing
• The call-by-need lambda calculus
• The Call-by-Need Lambda Calculus, Revisited
• Call-by-need, neededness and all that

Cited in

(4)

• Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
• Positive focusing is directly useful
• IMELL cut elimination with linear overhead
• Mirroring call-by-need, or values acting silly

This page was built for publication: Useful Open Call-By-Need

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6124931)