Call-by-need, neededness and all that

DOI10.1007/978-3-319-89366-2_13MaRDI QIDQ1652986zbMATH OpenOpenAlexFDO

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

Publication date 17 July 2018

Copyright license Creative Commons Attribution 4.0 International

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

Mathematics Subject Classification ID

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

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.

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

Cited in

(10)

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

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)