# Looking for a supervisor? (BSc, MSci)

I am happy to supervise any interesting project as long as it involves some serious programming. My personal preferences are functional languages (like Haskell) but I think you can do functional programming in any language :-). Most important is (sustained) enthusiasm on your side. Also I think it is essential to start programming early and not to delay this using the excuse that one has to do some research first.

In my research I am interested to explore the connection between mathematical reasoning and programming. One tool to do this is Type Theory, which is at the same time a programming language and a language to do mathematical constructions. There exists a number of implementations of Type Theory, the one I prefer is called Agda.

Since you may not know Agda I will organize a tutorial for Agda early in the year. However, if you are keen you are encouraged to download Agda and play around with it even before you start your project. Also there is a fair amount of support available via Researchers and PhD students in the FP lab.

Here is a list of possible topics using Agda, but feel free to propose your own:

1. Binary Arithmetic.
Implement fixed sized binary arithmetic in Agda and prove it correct. Starting point would be positive integers moving on to integers (2s complement) and potentially even floating point.
2. Combinatory logic is a very simple programming language. In this project I propose to explore programming in SK, leading up to writing a self-interpreter for SK and proving it correct.
3. Formalize formal languages: e.g. finite automata and regular languages and show the equivalence.
4. Propositional logic
Establish some basic results about classical and intuitionistic propositional logic: e.g. decidability and the negative translation.
5. Sorting algorithms
Show the correctness of various sorting algorithms in Agda
6. Basic combinatorics
Formally verify some basic combinatorics, like with the Pigeon Hole Principle or the theorem of friends and strangers.

Thorsten Altenkirch