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.

Advanced type systems

Static type checking can detect programming errors before a program is even executed. In the simplest case, type checking makes sure that we don’t try to multiply a number with an array of strings or similar silly things. More advanced type systems, for example in the Rust programming language, can ensure that low-level programs deal with memory safely and efficiently.

I am working on similar advanced type systems for reactive programming languages, which are languages for implementing programs that continuously interact with their environment (e.g. robots, web servers, GUIs, games etc.). The type system ensures that these reactive programs will run efficiently and safely. There are a number of possible projects in this area:

• Implement a reactive programming language with such an advanced type system. There are two different approaches: Either (1) you can implement it as a stand-alone language, or (2) you can implement it as part of an existing language (e.g. Haskell, F#, Scala).
  1. For this you will have to implement a parser, a type checker, and an interpreter for the language. 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…).
  2. This requires some tricks to hijack the type system of the host language (Haskell/F#/Scala/…) to adequately represent the reactive programming language. The benefit is that programs in your new language can make use of the host language’s features and libraries.
• Extend a functional programming language (e.g. Haskell, F#, Scala) with a library for efficient and safe reactive programming. This will likely require the use of advanced type system features of the implementation language.

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:

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