All functional languages need closures. Closure-conversion is a compiler transformation that embeds static code for creating and manipulating closures into the program, avoiding the need to do this at run-time. For call-by-value languages, closure-conversion has been the focus of extensive studies concerning both extensional features, such as type preservation and contextual equivalence, and intensional ones, such as space usage. Unfortunately, non-strict languages have been neglected in these studies. This paper aims to fill this gap.

First, we present a big-step semantics for both a call-by-name and a call-by-need language which explicitly capture the construction of closures at run-time. Next, we present type-preserving closure-conversions for these two non-strict languages that embed the construction of closures in programs of a target language. Despite the non-strict source of our languages, we show that closures must be created eagerly, which requires a strict notion of product in the target language. We extend logical relation techniques used to prove compiler correctness for call-by-value languages, to apply to non-strict languages, too. In doing so, we identify important properties for reasoning about memoization with an explicit heap.