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 V. Interestingly, system V also allows to syntactically identify all the weak-head needed redexes of a term.
CITATION STYLE
Kesner, D., Ríos, A., & Viso, A. (2018). Call-by-need, neededness and all that. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10803 LNCS, pp. 241–257). Springer Verlag. https://doi.org/10.1007/978-3-319-89366-2_13
Mendeley helps you to discover research relevant for your work.