Together with our collaborators, the SE group will present 5 (very) different papers at this year’s International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA 2025), matching the current highscore for most papers presented at this toplevel conference.

• Compiling Classical Sequent Calculus to Stock Hardware
• The Simple Essence of Monomorphization
• Tracing Just-in-time Compilation for Effects and Handlers
• Dynamic Wind for Effect Handlers
• The Simple Essence of Overloading

This year’s OOPSLA is co-located with the International Conference on Functional Programming (ICFP 2025), where we will present one additional paper.

• Multiple Resumptions and Local Mutable State, Directly

Furthermore, our student compiler engineer Marvin Borner
Student Compiler EngineerMarvin Borner will present his Bachelor thesis on Optimal Effects at the ICFP Student Research Competition (ICFP SRC).

Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation

Compiler intermediate representations have to strike a balance between being high-level enough to allow for easy translation of surface languages into them and being low-level enough to make code generation easy. An intermediate representation based on a logical system typically has the former property and additionally satisfies several meta-theoretical properties which are valuable when optimizing code. Recently, classical sequent calculus, which is widely recognized and impactful within the fields of logic and proof theory, has been proposed as a natural candidate in this regard, due to its symmetric treatment of data and control flow. For such a language to be useful, however, it must eventually be compiled to machine code. In this paper, we introduce an intermediate representation that is based on classical sequent calculus and demonstrate that this language can be directly translated to conventional hardware. We provide both a formal description and an implementation. Preliminary performance evaluations indicate that our approach is viable.

More about this publication

The Simple Essence of Monomorphization

Monomorphization is a common implementation technique for parametric type-polymorphism, which avoids the potential runtime overhead of uniform representations at the cost of code duplication. While important as a folklore implementation technique, there is a lack of general formal treatments in the published literature. Moreover, it is commonly believed to be incompatible with higher-rank polymorphism. In this paper, we formally present a simple monomorphization technique based on a type-based flow analysis that generalizes to programs with higher-rank types, existential types, and arbitrary combinations. Inspired by algebraic subtyping, we track the flow of type instantiations through the program. Our approach only supports monomorphization up to polymorphic recursion, which we uniformly detect as cyclic flow. Treating universal and existential quantification uniformly, we identify a novel form of polymorphic recursion in the presence of existential types, which we coin polymorphic packing. We study the meta-theory of our approach, showing that our translation is type-preserving and preserves semantics step-wise.

Live Demonstration More about this publication

Tracing Just-in-time Compilation for Effects and Handlers

Effect handlers are a programming language feature that has recently gained popularity. They allow for non-local yet structured control flow and subsume features like generators, exceptions, asynchronicity, etc. However, implementations of effect handlers currently often sacrifice features to enable efficient implementations. Meta-tracing just-in-time (JIT) compilers promise to yield the performance of a compiler by implementing an interpreter. They record execution in a trace, dynamically detect hot loops, and aggressively optimize those using information available at runtime. They excel at optimizing dynamic control flow, which is exactly what effect handlers introduce. We present the first evaluation of tracing JIT compilation specifically for effect handlers. To this end, we developed RPython-based tracing JIT implementations for Eff, Effekt, and Koka by compiling them to a common bytecode format. We evaluate the performance, discuss which classes of effectful programs are optimized well and how our additional optimizations influence performance. We also benchmark against a baseline of state-of-the-art mainstream language implementations.

More about this publication

Dynamic Wind for Effect Handlers

Effect handlers offer an attractive way of abstracting over effectful computation. Moreover, languages with effect handlers usually statically track effects, which ensures the user is aware of all side effects different parts of a program might have. Similarly to exception handlers, effect handlers discharge effects by locally defining their behavior. In contrast to exception handlers, they allow for resuming computation, possibly later and possibly multiple times. In this paper we present a design, formalization, and implementation for a variant of dynamic wind, that integrates well with lexical effect handlers. It has well-defined semantics in presence of arbitrary control effects in arbitrary places. Specifically, the behavior of capturing and resuming continuations in the pre- or postlude is well-defined and respects resource bracketing. We demonstrate how this features can be used to express backtracking of external state and finalization of external resources.

More about this publication

The Simple Essence of Overloading: Making ad-hoc polymorphism more algebraic with flow-based variational type-checking

Type-directed overload resolution allows the programmers to reuse the same name, offloading the work on the type-checker to disambiguate and resolve the overload. Since many programming languages implement overload resolution by performing backtracking in the type checker, it is commonly believed to be incompatible with Hindley-Milner-style type systems. In this paper, we present an approach to overload resolution that combines insights from variational type-checking and algebraic subtyping. We formalize and discuss our flow-based variational framework, which captures the essence of overloads by representing them as choices. This way, it cleanly separates constraint collection, constraint solving, and overload resolution. We believe our framework not only gives rise to more modular and efficient implementations of type-checkers, but also serves as a simpler mental model and paves the way for improved error messages.

More about this publication

Multiple Resumptions and Local Mutable State, Directly

While enabling use cases such as backtracking search and probabilistic programming, multiple resumptions have the reputation of being incompatible with efficient implementation techniques, such as stack switching. This paper sets out to resolve this conflict and thus bridge the gap between expressiveness and performance. To this end, we present a compilation strategy and runtime system for lexical effect handlers with support for multiple resumptions and stack-allocated mutable state. By building on garbage-free reference counting and associating stacks with stable prompts, our approach enables constant-time continuation capture and resumption when resumed exactly once, as well as constant-time state access. Nevertheless, we also support multiple resumptions by copying stacks when necessary. We practically evaluate our approach by implementing an LLVM backend for the Effekt language. A performance comparison with state-of-the-art systems, including dynamic and lexical effect handler implementations, suggests that our approach achieves competitive performance and the increased expressiveness only comes with limited overhead.

More about this publication

Publications