by Philipp Schuster, Jonathan Immanuel Brachthäuser, and Klaus Ostermann

In European Symposium on Programming (ESOP 2022), 2022.

This publication is related to the Compiling with Continuations research project.

Abstract

Regions are a useful tool for the safe and automatic management of scarce resources. Due to their scarcity, resources are often limited in their lifetime which is associated with a certain scope. When control flow leaves the scope, the resources are destroyed. Exceptions can non-locally exit such scopes and it is important that resources are also destroyed in this case. Continuation-passing style is a useful compiler intermediate language that makes control flow explicit. All calls are tail calls and the runtime stack is not used. It can also serve as an implementation technique for control effects like exceptions. In this case throwing an exception means jumping to a continuation which is not the return continuation. How is it possible to offer region-based resource management and exceptions in the same language and translate both to continuation-passing style? In this paper, we answer this question. We present a typed language with resources and exceptions, and its translation to continuation-passing style. The translation can be defined modularly for resources and exceptions – the correct interaction between the two automatically arises from simple composition. We prove that the translation preserves well-typedness and semantics.

News