Call-by-need, neededness and all that

DOI10.1007/978-3-319-89366-2_13zbMATH Open1504.68033arXiv1801.10519OpenAlexW3104952256MaRDI QIDQ1652986FDOQ1652986

Authors: Delia Kesner, A. Ríos, Andrés Viso 

Publication date: 17 July 2018

Abstract: We show that call-by-need is observationally equivalent to weak-head needed reduction. The proof of this result uses a semantical argument based on a (non-idempotent) intersection type system called $mathcalV$. Interestingly, system $mathcalV$ also allows to syntactically identify all the weak-head needed redexes of a term.

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

Recommendations

• The call-by-need lambda calculus
• Reasoning about call-by-need by means of types
• The call-by-need lambda calculus
• Small-step and big-step semantics for call-by-need
• The Call-by-Need Lambda Calculus, Revisited

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Cited In (10)

• Tight typings and split bounds, fully developed
• The spirit of node replication
• Reasoning about call-by-need by means of types
• Title not available (Why is that?)
• Node Replication: Theory And Practice
• Normalization by Evaluation for Typed Weak lambda-Reduction
• Formal verifications of call-by-need and call-by-name evaluations with mutual recursion
• On the value of variables
• Formal verification of the correspondence between call-by-need and call-by-name
• Useful Open Call-By-Need

This page was built for publication: Call-by-need, neededness and all that

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