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.
Tue 19 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
18:00 - 19:00
|A Type-Safe Structure Editor Calculus|
Christian Godiksen Department of Computer Science, Aalborg University, Thomas Herrmann Department of Computer Science, Aalborg University, Hans Hüttel Department of Computer Science, Aalborg University, Mikkel Korup Lauridsen Department of Computer Science, Aalborg University, Iman Owliaie Department of Computer Science, Aalborg UniversityMedia Attached
|Strictly Capturing Non-Strict Closures|
Zachary Sullivan University of Oregon, Paul Downen University of Oregon, USA, Zena M. Ariola University of Oregon, USAMedia Attached