We are looking forward to working with you on your thesis project (in German or English)!
Our group offers a range of open thesis topics in the general area of software engineering or programming languages.
We also welcome your own ideas, especially if they are in scope of our research topics.
If you are interested in pursuing a thesis with our group, please send us an email with the following information:
a brief description of the kind of work you are interested in (e.g. more theoretical, more practical, a programming task, ...)
your level of knowledge of the theory or implementation of programming languages (if any)
a current transcript of your grades
potentially relevant skills you acquired outside of university
Adding two numbers and adding (concatenating) two strings feels similar. It is only logical that both functions should be called the same. Normally two functions with the same name raise an error from the compiler. Function overloading enables the user to call functions that solve the same problem by the same name. The tradeoff is a more complex compiler that has to analyze the function signatures to find out which function is actually meant. This is called overload resolution. This master’s thesis explores augmenting the sequent calculus compiler with an overload resolution version derived from a paper by Jiří Beneš and Jonathan Immanuel Brachthäuser. Instead of exploring all possible combinations of function calls this paper proposes an approach that can copy the type constraints and tag them with different call choices accelerating the overload resolution.
Modern functional languages rely heavily on parametric polymorphism, allowing data structures and algorithms to be defined generically over arbitrary types. To eliminate the overhead of boxing and enable further optimizations, compilers typically employ monomorphization, which is the process of generating type-specialized copies of generic definitions. This thesis extends the Sequent Calculus Compiler (SCC), a research compiler whose intermediate representation is grounded in Gentzen’s classical sequent calculus, with first-class support for parametric polymorphism across both the Fun surface language and the Core IR. Currently, SCC supports only a limited form of polymorphism for data and codata types, resolved implicitly during type checking with no polymorphism at the term level. We address this by extending Fun and Core with structural type parameters and adapting the flow-directed monomorphization algorithm of Lutze, Schuster, and Brachthäuser (2025) to the sequent calculus setting, realizing it as a dedicated Core-to-Core pass that must account for the symmetric treatment of producers and consumers inherent to the sequent calculus.
Modelling various linguistic phenomena such as quantification and scope together is challenging, since different effects are typically modeled using different notations and rules. Continuations have been used to represent these phenomena, but as models grow in complexity, it becomes difficult to compose effects or verify examples without manually transcribing and evaluating them.
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.
Continuous Integration (CI) is a common best practice in software development.
This practice dictates, that among other factors, developers should commit early and often and receive feedback about their work as soon as possible.
In order to be effective in a large scale software development environment and to reap all the benefits that come with it, the CI pipeline has to be designed in a certain way and all stakeholders involved need to be instructed.
Partial type signatures are type signatures allowing wildcards in their definition. These wildcards are placeholders for other types which are inferred at compile-time. By using these wildcards, a programmer is able to annotate parts of a type signature manually and let the typer infer the rest. Therefore partial type signatures allow us to omit potentially long and complex parts of a type annotation while providing more restrictions to the type than without any annotation.
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.
Ordinary wisdom says that the individual tests in a testsuite should be independent of each other.
That is, each test should be able to run independently of any other test, and in any order.
This independence allows the testsuite driver to execute tests in parallel and easily summarize the results using a tests passed / tests failed metric.
Viele der Lehrmaterialien welche wir in der Lehre verwenden bestehen aus nicht interaktiven Skripten und Foliensätzen.
Aber die Inhalte der Informatik, under gerade auch der Programmiersprachentheorie, eignen sich besonders gut für eine interaktive Präsentation.
Durch eine interaktive Präsentation können auch sehr abstrakte Inhalte greifbar und verständlich gemacht werden.
So wird zum Beispiel häufig auf Animationen und interaktive Graphiken zurückgegriffen, um die Ausführung von Algorithmen zu veranschaulichen.
Im Rahmen dieser Bachelorarbeit wollen wir einige unserer Lehrmaterialien um interaktive Elemente ergänzen.
Einige konkrete Beispiele die wir gerne umsetzen würden sind:
Supercompilation is a compile-time optimization technique which uses partial-evaluation in order to generate an optimzed version of the program.
Supercompilation is known to generate significant speedups and to subsume various other optimization techniques.
The downsides of supercompilation are potentially huge increases in both compile-time and binary size.
Highcharts is a Javascript library for visualizing data. The purpose of this thesis
is to develop an adapter of Highcharts for Scala, such that data in the Scala runtime
can be visualized with the same ease as with dedicated data science languages such
as Mathlab or R.
Im Bereich der Entwicklung von Steuergerätesoftware kommen als Zielplattformen sowohl Gerätehardware als auch entsprechende Emulatoren zum Einsatz. Deren Verwendung ist vielfach kostenintensiv und für proprietäre Systeme oft mit einem Lock-in ohne Möglichkeiten der Erweiterung oder der Integration mit anderen Systemen verbunden. Der Einsatz von Fat Client Software erschwert darüber hinaus deren externe Verwendung zum Beispiel durch Testingenieure an Offshore-Standorten. Schließlich ist die Skalierbarkeit von Tests auf physischen Steuergeräten oder Fat Client Emulatoren stark eingeschränkt.
