Patrick Bahr IT University of Copenhagen

Project Supervision

If you are interested in having me as a superviser 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 master’s theses, bachelor 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:

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.