Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Tue 19 Jan 2021 18:30 - 19:00 at PEPM - Session 5 Chair(s): Torben Mogensen

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
Session 5PEPM at PEPM
Chair(s): Torben MogensenDIKU, University of Copenhagen

Live stream: https://www.youtube.com/watch?v=VJZcAtvGOyE

18:00
30m
Research paper
A Type-Safe Structure Editor Calculus
PEPM
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 University
Media Attached
18:30
30m
Research paper
Strictly Capturing Non-Strict Closures
PEPM
Zachary SullivanUniversity of Oregon, Paul DownenUniversity of Oregon, USA, Zena M. AriolaUniversity of Oregon, USA
Media Attached