March 16, 2026

Free Deduction Process Calculus

In sequent-style proof systems, natural deduction combines introduction and elimination rules, while Gentzen’s LK is defined by dual introduction forms. The λ-calculus and λμ̃-calculus capture the computational essence of normalization in these frameworks. However, there are also logical systems like Parigot’s “Free Deduction” (FD) which rely exclusively on elimination rules. While the term assignment system and semantics of such a calculus can be understood in terms of its translation to either ND or LK, we lack a standalone semantics for such a framework.

July 11, 2023

Multiple Return Values in Effekt

Multiple return values in functions have long been regarded as a powerful feature in programming languages, enabling concise and expressive code. However, not all programming languages support this feature natively. Instead, most languages emulate multiple return values only via tuples. In the case of dynamically typed languages like Common Lisp multiple return values are supported but the dynamic handling may cause headaches: (type-of (values x y z)) is the same as (type-of x). This master thesis delves into designing and implementing multiple return values in the Effekt language. The thesis introduces native support for multiple return values in Effekt, exploring their significance and potential impact on software development.

May 21, 2026

Linear Continuations in SCC

The Sequent Calculus Compiler (SCC) uses sequent-calculus-based intermediate representations to compile a functional programming language to native machine code. Within the SCC, control flow is explicitly encoded using consumers. A continuation is a consumer that represents the remainder of a computation. In standard functional programs, each continuation is used linearly, i.e. exactly once. However, the SCC also supports control operators that break this linearity assumption. This thesis investigates how to statically track the linearity of continuations and exploit it to generate more efficient machine code, reducing both runtime overhead and memory usage. To achieve that, the memory allocation mechanisms are extended for linear usage of data. In this work, these improvements are only applied specifically to continuations, but serve as a foundation for more general use cases.

March 19, 2026

Constant-Time Reference Counting in Effekt

Efficient memory management is a central challenge for programs that allocate and discard large data structures at runtime. In garbage-collected languages, reclaiming such memory can introduce significant overhead, causing load spikes and observable pauses in execution. To address this issue, we investigate alternative memory management strategies using the Effekt programming language as an experimental platform.

October 30, 2025

Effekt Chez Scheme

The Effekt language, a language supporting lexical effects and handlers, uses several intermediate representations (IR) during compilation. One of them uses continuation passing style (CPS). In this thesis, a new compilation strategy is explored, using this CPS IR and compiling it to Chez Scheme. CPS relies heavily on tailcalls, so we expect this strategy to lead to improved performance compared to other backends of Effekt which use the CPS IR, due to Chez Scheme’s support of tailcall optimization. Compared to backends using other IRs, we expect better performance because of the optimizations allowed by the CPS IR. All while supporting the same or more features as the other backends, including bidirectional effects and reentrant continuations.

October 1, 2025

Compiling with Arrays to CUDA

Array programming languages have become increasingly relevant in many domains, especially in machine learning and scientific computing. Array programming offers concise, declarative syntax with high-level operations on arrays. High-level operations on arrays enable implicit parallelism of computations; however, mainstream systems typically trade off compile-time shape guarantees for performance on accelerators.

September 1, 2025

Bringing Classical Sequent Calculus to The Web

When choosing a compiler intermediate representation, both its intrinsic properties and the availability of compilation targets must be considered. It should admit an easy translation from a rich surface language, be type-safe, and make strong meta-theoretical guarantees. AxCut has recently been proposed in this field, meeting these requirements. It inherits the logical properties from classical sequent calculus and can elegantly model complex control flow. However, an intermediate representation is only relevant if it can be used to generate machine code for the architectures of interest. While AxCut can already be compiled to x86-64 and AArch64, one increasingly important target is currently missing: the web. In this thesis, we enable users of AxCut to target browsers. We therefore provide a translation from AxCut to WebAssembly. WebAssembly strongly differs from the classical architec tures AxCut was originally designed for. Despite this, we reproduce the semantics while matching the native code in terms of the number and types of jumps. To ensure correctness, our implementation was tested extensively and enforces certain invariants using dependent types. Preliminary performance evaluations show that performance is not yet comparable to the native code, but we provide potential solutions for this.

March 18, 2025

A Modern Implementation of Cut Elimination for Classical Sequent Calculus

The symmetrical properties of the sequent calculus make it an interesting base for functional programming languages. In contrast to the prevalent base lambda calculus, it allows for an equivalent treatment of terms producing information and evaluation contexts. In this thesis, we have constructed and implemented a term language for the sequent calculus, along with its cut-free fragment. We further present a normalization function that evaluates statements to their cut-free form, utilizing cut elimination and hereditary substitution. Thereby, it lends itself as a compiler intermediate language, shifting computation from runtime to compile-time, and optimizing program execution.

February 21, 2025

Optimal Effects

When evaluating functional programs, there are various strategies for reducing expressions. A strategy is Lévy-optimal if it never does unnecessary work such as duplicating terms that are later erased. To implement this efficiently, graphical representations like Interaction Nets can be used to encode the sharing of duplicated terms. Beyond optimality, Interaction Nets provide elegant solutions for parallelization and distributed computing, making them an attractive backend for programming languages. Side effects such as file I/O are rarely discussed in the context of optimal reduction, despite their necessity for real-world applications. In this thesis, we will therefore analyze and formalize existing implementations, and design and implement an optimal runtime with side effects.

October 23, 2024

Kompilierung von Effekthandlern mit Interaktionskombinatoren

In dieser Bachelorarbeit wird beschrieben wie Bend, eine Programmiersprache, die auf Interaktionskombinatoren basiert und noch in Entwicklung ist, als Backend des Effekt Kompilierers hinzugefügt wird. Bend kompiliert zu HVM, was für Higher-order Virtual Mashine steht. HVM implementiert die von Lafont [5] entworfenen Interaktionskombinatoren. Bend kann einige Lambda-Terme in von Levy [7] definierter optimaler Zeit berechnen und sehr leicht mehrere Berechnungen parallel durchführen. Deshalb hoffen wir mit Bend als Backend die Laufzeit von Effekt in einigen Programmen stark zu reduzieren.

October 23, 2024

Compiling classical sequent calculus to LLVM

This thesis aims to provide a way to translate classical sequent calculus to the LLVM intermediate representation to utilize the LLVM toolchain and achieve greater performance than compiling directly to machine code. We provide examples of how this translation works, what the resulting optimized version looks like and how and why we implemented a custom memory allocater to suit our needs. We show how to evaluate the resulting programs and how we test the validity of the translation. Finally we benchmark our approach against other programming languages and compare the resulting performance.

July 11, 2023

Probabilistic Effekt

Inference programming - the adaptation of inference algorithms to a particular model or problem - is difficult in languages that do not deal with side effects or do not handle side effects properly due to their nature of relying on effectful computation. In functional programming, monad transformers are the most common approach to control side effects. However, this makes it difficult to customise such algorithms. Effects and effect handlers on the other hand introduce another possibility to deal with programmable inference. This thesis will demonstrates this idea by developing three inference patterns (Metropolis-Hastings, slice sampling and rejection sampling) using the language Effekt. The result is a more user-friendly way to adapt and combine parts of these algorithms

July 11, 2023

Is Effekt Fast Yet

Alle Programmiersprachen besitzen eine gemeinsame Schnittmenge der grundlegenden Abstraktionen. Durch einen Kompiler oder Interpreter werden die Abstraktionen in Maschinencode umgesetzt und dann ausgeführt. Je besser diese Umsetzung optimiert ist, desto performanter ist die Ausführung des Programmes. Im Paper Are-We-Fast-Yet [ 5 ] werden 9 Microbenchmarks entwickelt, welche in moderat komplexen Programmen jeweils bestimmte Bereiche dieser Core Language testen. Die Benchmarks werden in verschiedene Programmiersprachen implementiert und die Ausführung auf Zeit gemessen. Anhand der Ergebnisse lässt sich eine generelle Aussage über die Performanz einer Programmiersprache, beziehungsweise Kompilers/Interpreters machen.

May 23, 2023

Reactive: Design and Implementation of a synchronous reactive programming library in Effekt

Reactive systems are an important part of everyday programming. Still, the implementations of such reactive systems differ hugely, which has a major impact on the style and reliability of reactive programs. The main approach to implementing reactivity and parallelism in the industry is to use multi-threading. This approach often leads to non-deterministic behavior. Additionally, programming languages often need extra implementations for reactivity and parallelism to support multi-threading. Languages such as Effekt eradicate the need for additional reactive system language support, by implementing algebraic effects. With algebraic effects, it is possible to implement a vast amount of programs, including reactive systems. In this work, we present Reactive, a library for the programming language Effekt. Reactive uses algebraic effects to implement reactivity and parallelism in direct style. The ability to write programs in direct style leads to more readable code, as it appears to be sequential, while the control flow is handled with algebraic effects. Reactive defines a synchronous execution model, by interleaving waiting parts of the program. The synchronous approach of the library makes decisions over the execution flow of the program deterministic. Parallelism and reactivity are decoupled by using different effects and handlers. With schedulers, Reactive creates the ability to run parts of a program in parallel. Reactive implements different schedulers, which handle the control flow of the program by enforcing rules. Such rules can be the termination of parts of the program when another has already stopped. The awaiting of an event is done by polling an environment in a busy wait loop, which can be interleaved with other parts of the program. Additional to the Effekt implementation, this thesis implements the ability to wait for JavaScript events inside the Effekt language.

January 5, 2023

Mutable State in a Language with Effect Handlers

Effekt is a functional programming language developed for research on algebraic effects and handlers. Aside from algebraic handlers, Effekt also features side effects in form of mutable state using region-based memory management. The Effekt compiler has multiple backends, one of which targets the LLVM Intermediate Representation. The LLVM-IR can be compiled to an executable file with many optimization passes on the way. The LLVM backend of Effekt covers only a subset of Effekt’s features. As part of this thesis, we extend the LLVM backend by support for mutable state.

February 24, 2022

Abstract-Interpretation-Based Language Server for Python

Most IDEs for Python development follow traditional code analysis approaches that are known to work well for statically-typed languages such as Java or C++. A lot of modern Python code is untyped, and these conservative tools tend to assign the “Any” type for variables that do not have explicit type annotations. However, programmers are usually able to deduce types (and often concrete values) by looking at surrounding code and jumping through function definitions and call sites.

October 28, 2021

Second-class modules for the Effekt programming language

Effekt is a research programming language that features a lightweight implementation of effects and handlers. As part of this thesis, the language was extended with second-class modules and related functionalities. These new features allow programmers to define modules and abstract them with interfaces. Also, the module system aims to strengthen the interplay between effects and modules. Both concepts share common characteristics, paving the way for potential future unification. This work examines those possibilities and provides insights into the relationship of modules and effects.

July 27, 2021

Making Fragment Based Code Distribution Practical

Package managers for programming languages are becoming more and more prevalent with only few languages not having one. The packages that one can add to a project with these tools are stored in an online repository, where users can share their work and make it available to other developers. This has led to huge increase in productivity. Fragnix is a prototype that is built around the idea of not sharing huge packages, that can contain several module files but rather the smallest possible unit of distribution: single functions. This thesis explains what was necessary to turn the Fragnix prototype from a tool, that could extract single definitions from Haskell modules into its own files, into a package manager, that transmits these files over the internet to integrate them in a user’s project.

April 1, 2021

Build Systems à la Carte with Effect Handlers

Algebraic effect handlers have been gaining attention in programming language re- search. They offer a new, abstract way of control flow. In this thesis we do a case study on reproducing a Haskell framework for build systems in Effekt, a new programming language with support for algebraic effect handlers.

February 10, 2021

Entwicklung eines Frontends für eine Datenbank an Haskell-Code-Snippets

Diese Bachelorarbeit befasst sich mit der Entwicklung eines Frontends für eine Datenbank, die Codeausschnitte der Programmiersprache Haskell beinhaltet. Das Frontend soll hier eine Webseite sein, die ein Nutzer im ersten Schritt auf seinem System installieren kann und die in einem weiteren Schritt auch öffentlich zugänglich gemacht werden kann.

November 30, 2019

Fragnix-Gui Creating a declaration editor for an alternative software sharing platform for Haskell

Building upon the existing Fragnix tool [fragnix], which slices a Haskell program into its declarations and enriches them with metadata, this thesis envisions a software sharing ecosystem based on sharing single declaration slices. Such an ecosystem could offer improvements in terms of performance, dependency tracking and maintenance and help with the prevention of effort duplication. A declaration editor is chosen as the next step towards realizing the tools for this slice sharing ecosystem. Using Haskell in the back-end and Elm in the front-end, prototypes for navigating code in form of slices are developed. A layout based on code-folding and in dentation proves to be most promising and is used for implementing the back-end foundations for editing and the ability to edit the text of declarations. The implementation of the remaining editing features is left for future work.

October 10, 2019

A Comparison of Probabilistic Programming Languages

The goal of this bachelor thesis was to investigate the differences between probabilistic programming languages. Therefore a case study was performed. We represented a hidden markov model and implemented inference on it with two probabilistic programming languages, WebPPL and Pyro. WebPPL following a functional approach as well as Pyro that sticks to an imperative programming paradigm succeeded in representing the hidden Markov model. Concerning the inference on the hidden markov model critical spots such as dealing with state depending models were revealed. We came to the conclusion that there exists a balancing problem between a generalization and a highly individual implementation of inference algorithms for probabilistic program- ming languages. The bachelor thesis is interesting for Bachelor or Master students of computer science and related courses of studies. It is also in- teresting for anybody dealing with probabilistic models and inference on them.

October 5, 2019

Portierung eines Visualisierungs-Frameworks von C# nach Python

Um die kundenorientierte Reichweite eines Unternehmens zu vergrößern, welches Softwareschnittstellen anbietet, ist es notwendig, diese Schnittstellen für verschie- dene Programmiersprachen bereitzustellen. Um dabei den Aufwand gering zu halten, soll großteils nur in einer Sprache entwickelt werden und die Software soll anschließend automatisch in andere Sprachen übersetzt werden. Die Firma yWorks entwickelt dafür das Übersetzungsprogramm Blunter. Unter Verwendung des Blunters soll das von yWorks nach dem Model-View-Controller (MVC)-Pattern programmierte Visualisierungs-Framework yFiles nach Python portiert werden. Für die graphische Darstellung in Python wird ein externes Graphical User In- terface (GUI)-Framework verwendet, welches bereits beim Übersetzungsprozess automatisch in die Python-Portierung integriert wird.

September 18, 2019

Performance-Analyse und -Optimierung der Ausgabe eines C#-zu-Python-Quellcodeübersetzers

Im Zuge des Tübinger Software-Projekts (TSPs) 2018/19 wurde in Zusammenarbeit mit der yWorks GmbH (yWorks) die neue Version 3.0 des Quellcodeübersetzers Blunter entwickelt. Dadurch ist das Programm nun in der Lage, ein gegebenes C#-Projekt in ein Python-Projekt zu übersetzen.

January 5, 2018

Strong Reduction in Lambda Calculus and its Use in Program Optimization

Program optimization by compilers is important - especially for functional programming languages. Yet at least parts of it remain a ”black art”, as Simon Peyton Jones describes the inlining technique in [0], full of compromises and heuristics. The problem, known as code bloat, is that optimization techniques might actually make performance worse by inlining too much, blowing up the code size.

December 12, 2017

Testen von Integrierten Entwicklungsumgebungen

In dieser Bachelorarbeit geht es um das automatische Testen einer eigens programmierten integrierten Entwicklungsumgebung. Die Applikation wird in Qt/C++ programmiert und mittels des Testframeworks Squish getestet. Dabei wird zuerst im Allgemeinen auf Qt und Squish eingegangen. Darauf folgen Vorgehensweise und Entwicklungswerkzeuge. Im Anschluss wird die Applikation, welche Hypertext Phoenix genannt wird, beschrieben. Das letzte und längste Kapitel widmet sich komplett dem Testen. Hier wird auf allgemeine Themen wie Tests von Hypertext Phoenix mit Beispielen eingegangen. Abschluss dieses Kapitels bildet der Nutzen von Tests.

August 26, 2025

Six Papers at OOPSLA and ICFP 2025

February 23, 2025

Two Papers at OOPSLA 2025 R1

Together with our collaborators the SE group presents two (very) different papers at round 1 of this year’s International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA 2025 R1).

October 22, 2023

Three Papers at OOPSLA 2023

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).

August 28, 2023

Paper accepted for publication at OOPSLA 2023

Our paper “From Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect Handlers” (Marius Müller, Philipp Schuster
Teaching SpecialistPhilipp Schuster, Jonathan Lindegaard Starup, and Klaus Ostermann, Jonathan Brachthäuser
ProfessorJonathan Immanuel Brachthäuser) has been accepted for publication at the International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA 2023).

February 20, 2023

Paper accepted for publication at OOPSLA 2023

Our paper “Continuation-Passing to Direct Style: Typed and Tight” (Marius Müller, Philipp Schuster
Teaching SpecialistPhilipp Schuster, Jonathan Brachthäuser
ProfessorJonathan Immanuel Brachthäuser, and Klaus Ostermann) has been accepted for publication at the International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA 2023).

October 1, 2020

Paper accepted for publication at OOPSLA 2020

Our paper “Effects as Capabilities: Effect Handlers and Lightweight Effect Polymorphism” (Jonathan Brachthäuser
ProfessorJonathan Immanuel Brachthäuser, Philipp Schuster
Teaching SpecialistPhilipp Schuster and Klaus Ostermann
ProfessorKlaus Ostermann ) has been accepted for publication at the International Conference on Object Oriented Programming Systems Languages & Applications (OOPSLA, 2020).

July 25, 2020

Presentation at ICFP 2020

Philipp Schuster
Teaching SpecialistPhilipp Schuster presents the paper Compiling Effect Handlers in Capability-Passing Style at the International Conference on Functional Programming (ICFP) 2020 virtual event.

May 9, 2020

Two papers conditionally accepted at ICFP'20

Two papers of the effects research team have been conditionally accepted at the International Conference of Functional Programming 2020.

January 23, 2020

Paper accepted for publication in the Journal of Functional Programming

Our paper “Effekt: Capability-Passing Style for Type- and Effect-Safe, Extensible Effect Handlers in Scala” (Jonathan Brachthäuser
ProfessorJonathan Immanuel Brachthäuser, Philipp Schuster
Teaching SpecialistPhilipp Schuster and Klaus Ostermann
ProfessorKlaus Ostermann ) has been accepted for been accepted for publication in the Journal of Functional Programming (JFP).

March 25, 2019

Shonan Meeting on Programming and Reasoning with Algebraic Effects and Effect Handlers

Philipp Schuster
Teaching SpecialistPhilipp Schuster attends the Shonan meeting on “Programming and Reasoning with Algebraic Effects and Effect Handlers” from March 25 to 29, 2019.

March 14, 2019

Presentation at ESOP 2019

Former member Paolo Giarusso presents the paper Incremental λ-Calculus in Cache-Transfer Style at the European Symposium on Programming (ESOP) 2019 in Prague, Czech Rebuplic.

November 7, 2018

Presentation at OOPSLA 2018

Jonathan Brachthäuser
ProfessorJonathan Immanuel Brachthäuser presents the paper Effect Handlers for the Masses at the International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA) in Boston, MA, USA.

August 20, 2018

Presentation at Type-Driven Development 2018

Philipp Schuster
Teaching SpecialistPhilipp Schuster presents the functional pearl Typing, Representing, and Abstracting Control at Type-Driven Development 2018.

September 9, 2017

Presentation at Haskell Implementors Workshop

Philipp Schuster
Teaching SpecialistPhilipp Schuster presents An Experiment in Fragment-Based Code Distribution at the Haskell Implementors Workshop.

September 27, 2016

Workshop at HaL workshop

Philipp Schuster
Teaching SpecialistPhilipp Schuster presents Ten example uses of monads at Haskell in Leipzig workshop series.