Reasoning About Call-by-need by Means of Types

Abstract. 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.

• Type: Journal
• Year: 2016
• Where: FOSSACS
• Authors: Delia Kesner
• Keywords: FOSSACS 2016, Software Engineering