Project Supervision

If you are interested in having me as a supervisor for your research project, BSc project or MSc thesis, contact me via email. I am particularly interested in projects that involve compilers, type systems, functional programming, and formal verification.

You are strongly encouraged to form groups of two or three as group projects are much more likely to work out well and complete on time.

Project Ideas

Below are some ideas for MSc theses, BSc projects and other projects for students at the IT University of Copenhagen.

Compilers and type systems for functional reactive programming

Reactive systems are software systems that continuously interact with their environment. Such systems include control software for robots, web servers, graphical user interfaces, and games. Functional reactive programming is an approach to implement these systems using functional programming. In order to produce efficient code, such functional reactive programming languages have a more advanced type system compared to standard functional programming language. The design and implementation of these advanced type systems is an active area of research.

There are several options for a project in this area:

• Implement a functional reactive programming language as an embedded language of an existing language, e.g. Haskell, F#, Scala. This requires some tricks to hijack the type system of the host language (Haskell/F#/Scala/…) to adequately represent the type system of the reactive programming language. The benefit is that programs in your new language can make use of the host language’s features and libraries.
• Implement a compiler for functional reactive programming language (including a parser, a type checker, and code generator). This gives you maximal freedom to implement the language and do clever things with it (such as type inference, optimisations, more advanced type system features, more efficient memory management). A smaller project could also just focus on one particular aspect of the compiler, e.g. type inference.
• Use an existing functional reactive programming language to implement a non-trivial system, e.g. a GUI framework, a game, a library for generating smooth animations and visualisations. The aim of this project would be to evaluate how the non-standard type systems of these programming languages influence the development of such software.

Property-based testing

Property-based testing is an approach to testing where the programmer first writes properties that their program must satisfy (e.g. sorting a list twice produces the same result as sorting it once) and then uses a tool or library that tests these properties by generating random inputs. The goal of this project is to design and implement such a tool/library for reactive programming. Testing reactive programs is challenging, since they are highly interactive. A main challenge is designing a good language to express the properties that the programmer can test their programs against.

Correct-by-construction compilers

Compilers are complex pieces of software with subtle optimisations that are hard to get right. Getting it right is crucial since bugs will propagate to any software that has been built using a faulty compiler. However, compiler bugs are very difficult to spot with standard testing alone.

Alternatively, we might hope to formally verify that a compiler implementation works correctly according to its specification. One such approach is to derive the compiler directly from its specification: From a formal specification, the implementation of the compiler is derived by a series of calculation steps – similar to algebraic simplifications of arithmetic expressions. To avoid user errors in this process we use tools such as Coq or Agda that check for mistakes and automate easy steps of the calculation. However, these are generalist tools that make this process laborious and difficult to follow.

The goal of this project is to implement a tool that is able to check and partially automate the derivation of compilers from specifications.

Recent BSc and MSc theses

Below is a selection of theses that I have supervised in recent years:

• Sebastian Bue Bjørner. Automated Derivation of Correct Compilers, MSc Thesis, IT University of Copenhagen, 2024.
• Jean-Claude S. Disch and Asger L. Heegaard. Asynchronous FRP for Implementing GUIs, MSc Thesis, IT University of Copenhagen, 2024.
• Natalia Ixchel Rodas Ralda and Thor Christian Stenbæk. Implementation of a Polymorphic Functional Reactive Programming Language with Modal Types, MSc Thesis, IT University of Copenhagen, 2024.
• Alexander Berg and Emil Jäpelt. Implementing a Standalone Language for Asynchronous Modal FRP, MSc Thesis, IT University of Copenhagen, 2024.
• L. Jensen. Property Based Testing of Functional Reactive Programs using Linear Temporal Logic, MSc Thesis, IT University of Copenhagen, 2023.
• Emil Houlborg and Gregers Skat Rørdam. Asynchronous Rattus: A Functional Reactive Programming Language with Multiple Clocks, BSc thesis, IT University of Copenhagen, 2023.