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) enthusiam 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 most interested to explore the relation between reasoning and programming which is called the Curry Howard equivalence of propositions and types (and proofs and programs). If you have done G52IFR you should have already got a first taste of this. One means to use this in a final year project is to formalize a piece of Mathematics or theoretical Computer Science or verify a program using an interactive theorem prover. My favorite is Agda, a system from Sweden, which is somewhere in between Coq and Haskell. In the past year I have supervised a number of very successful (and a few not so successful) projects involving Agda.

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

Binary Arithmetic.
Implement fixed sized binary arithmetic in Agda and prove it correct. Starting point would be psoitive integers moving on to integers (2s complement) and potentially even floating point.
Normalisation by evaluation
This is a technique to compute normal forms for typed lambda calculus and combinatory logic. The goal of the project would be to implement normalisation function with its correctness proof in Agda for one or several calculi.
Push Down Automata and Context Free Langauges
The goal of this project is to formally develop this part of G52MAL: define PDAs and CFLs, prove the relationship, prove the pumping lemma for context free langauges and more.
Turing Machines and the Halting Problem
Formalize Turing Machines (or another complete computational formalism) and prove the undecidability of the Halting problem.
Containers and derivatives of datatypes
Formalize basic aspects of container theory in Agda, and investigate the derivative of datatypes.
Propositional logic
Establish some basic results about classical and intuitionistic propositional logic: e.g. decidability and the negative translation.
Sorting algorithms
Show the correctness of various sorting algorithms in Agda
Verified Haskell Prelude
Specify and verify functions from the Haskell prelude.
Basic combinatorics
Formally verify some basic combinatorics, starting with the Pigeon Hole Principle moving on to Ramsey theory.
Simplicial sets
Simplicial sets are the core to formally develop higher dimensional concepts in Type Theory. The project would involve formalizing simplicial sets in Agda and proving some basic results.

I am happy to organize an Agda Tutorial for students working on an Agda related project. However, this should not be used as an excuse to postpone working on your project.

Thorsten Altenkirch