Call-by-Need, Neededness and All That
Logic in Computer Science
2020-09-09 v2 Programming Languages
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 . Interestingly, system also allows to syntactically identify all the weak-head needed redexes of a term.
Keywords
Cite
@article{arxiv.1801.10519,
title = {Call-by-Need, Neededness and All That},
author = {Delia Kesner and Alejandro Ríos and Andrés Viso},
journal= {arXiv preprint arXiv:1801.10519},
year = {2020}
}