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 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
18:00 - 19:00
|A Type-Safe Structure Editor Calculus|
Christian GodiksenDepartment of Computer Science, Aalborg University, Thomas HerrmannDepartment of Computer Science, Aalborg University, Hans HüttelDepartment of Computer Science, Aalborg University, Mikkel Korup LauridsenDepartment of Computer Science, Aalborg University, Iman OwliaieDepartment of Computer Science, Aalborg UniversityMedia Attached
|Strictly Capturing Non-Strict Closures|
Zachary SullivanUniversity of Oregon, Paul DownenUniversity of Oregon, USA, Zena M. AriolaUniversity of Oregon, USAMedia Attached