We first develop a (semantical) characterization of call-byneed normalization by means of typability, i.e. we show that a term is normalizing in call-by-need if and only if it is typable in a suitable system with non-idempotent intersection types. This first result is used to derive a new completeness proof of call-by-need w.r.t. call-by-name. Concretely, we show that call-by-need and call-by-name are observationally equivalent, so that in particular, the former turns out to be a correct implementation of the latter.
CITATION STYLE
Kesner, D. (2016). Reasoning about call-by-need by means of types. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9634, pp. 424–441). Springer Verlag. https://doi.org/10.1007/978-3-662-49630-5_25
Mendeley helps you to discover research relevant for your work.