Together with our collaborators the SE group presents three different papers at this year’s International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA 2023).

• From Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect Handlers
• Back to Direct Style: Typed and Tight
• Getting into the Flow: Towards Better Type Error Messages for Constraint-Based Type Inference

From Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect Handlers

Jonathan Brachthäuser
Head of the SE research groupJonathan Immanuel Brachthäuser presents our work on connecting lexical scoping with dynamic regions.

To optimize the runtime cost of effect handlers, this paper presents the missing link in the pipeline to compile programs with lexical effect handlers to iterated continuation-passing style (CPS). Going to System F, existing optimizations and metatheoretical results can immediately be reused.

One key contribution of this paper is a translatation of lexical handlers into a region-based calculus, maintaining sufficient information about the nesting of handlers. With this information the CPS translation can decide how effects have to be lifted through handlers, i.e., which handlers need to be skipped, in order to handle the effect at the correct place.

More about this publication

Back to Direct Style: Typed and Tight

Marius Müller presents our work on translating programs from continuation-passing style back to direct style.

We examine the translation between continuation-passing style (CPS) and direct style (DS) of typed calculi. We explore two calculi with abstract machine semantics capable of non-trivial control flow, presenting type-preserving translations between them. The translations maintain precise operational correspondence and exhibit syntactic inverses, especially under trivial control flow conditions.

More about this publication

Getting into the Flow: Towards Better Type Error Messages for Constraint-Based Type Inference

Ishan Bhanuka presents our work on a principled approach towards more exhaustive type error locations.

Our approach utilizes algebraic subtyping to track data flow to generate detailed type error messages in constraint-based type systems. In particular, we explain type errors as faulty data flows, which programmers are already used to reasoning about. The generated error messages illustrate these data flows as sequences of relevant program locations.

We show that our ideas and algorithm are not limited to languages with subtyping, as they can be readily integrated with Hindley-Milner type inference.

More about this publication

Publications