Projects

My research interests are primarily mathematical, typically involving formal logic, category theory and the foundations of computer science. If you are interested in a mathematical project in these areas, please contact me directly.

Although my work is theoretical, and have over a decade of industry software development experience, and am happy to supervise programming projects. I suggest a few potential directions below, although I am open to discussing variations or similar projects. Students should be enthusiastic about coding, and producing a good quality software implementation. Only limited knowledge of the background mathematics should be required, and can be explored to the taste of the students involved.

All the projects are intended to be challenging, and therefore offering the scope for an impressive project assuming enough time and effort is invested.

Two Sum

Two Sum is the first problem on the Leetcode website, and is considered to be an easy problem. We are given an array of $n$ integers $A$ and a target value $\mathsf{target}$ , and are asked to find

i, j \text{ such that } 0 \leq i,j <n, i \neq j

and

A[i] + A[j] = \mathsf{target}

The input is guaranteed to contain a unique solution. As a follow-up we are asked to find a solution that runs in better than

\Omicron(n^2)

Solutions to both parts are straightforward, and many examples are available on the internet. The aim of this project is to study the performance of solutions to this simple problem, and generalisations thereof in an “efficient” systems programming language such as C, C++, Rust or Zig. A first step will be to compare the performance of the naive solution with the version with better asymptotic complexity on different datasets, and establish how they perform in practice.

Subsequent steps will involve generalising the original problem, or solutions, and studying the practical performance in detail, for example:

By dropping the requirement $i \neq j$
By generalising two sum to $n$ sum, looking for exactly $n$ values summing to the target.
By generalising to allow for multiple potential target values.
To generalise beyond the fixed requirement $A[i] +A[j] = \mathsf{target}$ .
Considering situations when some of the parameters such as the array length are known at compile time.
Exploring the impact of exploiting concurrency.

The project would be suitable for a student with an interest in programming and performance, and will develop a good understanding of how the performance characteristics of even simple code can be a complex topic in practice.

A Diagrammatic Programming Language

Design and implement a prototype programming language for describing two-dimensional diagrams and compiling them to produce the resulting diagram in a common graphics file format. The language should be suitable for developing large numbers of diagrams suitable for use in books and papers. The tool should be suitable for rendering string diagrams, many examples of which can be found in this paper.

The project is expected to be challenging, so students should manage the scope carefully, and add features incrementally to manage delivery risks. Features might include:

Primitives for describing diagram features
Sensible default behaviour combined with options for fine-tuning layouts
Methods for building up diagrams via composition and substitution from simpler parts
Code reuse features such as modules
A type system, and other support for identifying errors in diagrams and debugging
Programs should be described in text files as with any typical programming language, so they can be edited and version controlled using standard tools

This project would be suitable for a student interested in programming languages, and with strong programming skills.

Evaluation C Replacement Languages

There have emerged several systems programming languages, commonly referred to as “C replacement languages”, including:

Rust
Zig
Odin
C3

The aim of this project is to provide a careful comparison of the practical capabilities of these languages. This would be done by choosing a suitable small command line utility, and implementing it in C, and two potential replacements. In each case, the aim is to make idiomatic use of the languages in question, and produce a good quality implementation to enable fair comparisons.

Based on the practical work, the aim is to contrast these languages in the context of the code that was developed, potentially including:

Performance: Does the choice of programming language have any performance implications?
Expressiveness: Can the developer express their intent within the code, or is the design left implicit, or hidden in documentation or comments?
Clarity: Do the language features have implications for the clarity of the resulting code?
Ergonomics: Which language feature prove convenient for writing clear, concise code?
Correctness: Which language features prove important for reducing the scope for errors?
Ecosystem: How did the ecosystem of tools and libraries impact the development process?
Portability: How easy is it to support multiple platforms?
Other factors: Are there other factors that are important to consider when choosing between these languages? Examples might include human factors such as the developer community, educational literature or demand with employers.

The challenge will be to reach meaningful, well-justified, concrete conclusions, and avoiding becoming an emotive “which language is best” discussion.

Literature:

The natural starting point will be the online documentation for the chosen languages.
It will be useful to find some good quality code examples for the languages of interest, showing how experienced developers use them in practice.

This project will suitable a practically-minded student with an interest in programming and programming languages.

Games and SAT Solvers

The propositional satisfiability problem is the canonical example of an NP-complete problem. Generalising propositional logic leads to more expressive logics such as quantified Boolean logic (QBF), dependency quantified Boolean logic (DQBF), second order quantified Boolean logic (SOQBF), modal logic and the mu-calculus, each of which yields complete problems for well-known complexity classes. Many of these logics have available solvers that can be used to explore the practicalities of their satisfiability problem.

Another source of complete problems for complexity classes is to consider the problem of finding winning strategies for certain games and puzzles. The starting point for this project would be to explore this relationship from a practical point of view. Can appropriately chosen standard satisfiability solvers provide useful tools for finding winning strategies for games and puzzles? How well does this scale? What are the choices when encoding games as satisfiability problems?

This project might suit students with interests in either AI, logic or algorithms, with the direction taken adjusted to their interests.

Generic Game Solver

As well as being educational and fun to play, games are a flexible abstraction for describing different types of interaction and decision making. Many problems in computer science can naturally be phrased as a requirement for a winning strategy for a suitable game. The aim of this project would be to develop software that finds winning strategies for a general class of games. Aspects of the project could include:

Identifying a general class of games that has concrete games of interest as special cases.
Implementing one or more solution strategies for finding winning strategies.
Evaluating the scalability of the game solver as a general purpose problem solving tool.
Considering how to certify that a winning strategy has been found that can be validated independently.

The project would be suitable for students with interests in algorithm design or artificial intelligence.

A Turing Machine Compiler

Turing machines crop up in many parts of theoretical computer science. In some applications, such as the study of busy beaver numbers, it is useful to have a concrete Turing machine implementing a given program. See for example this paper showing that sufficiently big busy beaver numbers are, very loosely speaking, “outside the scope of formal mathematics”.

The aim of this project is to produce a compiler for a simple programming language, generating Turing machines as the target output. As a supporting goal, it will be necessary to implement a Turing machine simulator to run the output of the compiler. A stretch goal would be to optimise the number of states of the generated Turing machines, as this is of interest in applications.

This is primarily a programming project, but with some challenging design questions to address. It would suit a student interested in some combination of compilers, programmings languages and theory of computation.

A Bernays-Schönfinkel-Ramsey Class SAT Solver

The Bernays-Schönfinkel-Ramsey class is a decidable fragment of first-order logic, and is in fact NExpTime complete. The complexity of the satisfiability problem implies we will not be able to solve this problem efficiently in general, but does not preclude satisfactory performance on instances that might be of practical interest. The aim of this project is to implement and evaluate a satisfiability solver for this logic.

This project would suit a student with strong programming skills in a “fast” language such as C++ or Rust, although an implementation using a less obvious language could be considered.

Exploring the Weisfeiler-Leman algorithm

Colour refinement, and its generalisation the Weisfeiler-Leman algorithm are algorithms with connections to many areas including logic, linear programming, machine learning and the famous graph isomorphism problem. Intuitively these algorithms iteratively colour subsets of vertices of a graph as they extract more information about the relationships between different sets of vertices. There are several variations of this algorithm for different graph types such as directed or weighted graphs.

The aim of this project would be to explore programmatic aspects of variations of the Weisfeiler-Leman algorithm. This could be done in many ways, such exploring efficient implemenations of these algorithms, or visualisers of their behaviour.

Games on graphs

Similarly to the situation in logic, there are a vast number of games that can be played on graphs and graph like structures. Examples include pursuit evasion games such as cops and robbers, and graph theoretic variants of combinatorial games such as Nim. These games have many uses in mathematics and computer science, such as to study and quantify the combinatorial structure of graphs, or in connection with important algorithmic problems. Again, there are a variety of different directions a programming project could go in, such as automated solvers or AI techniques for playing these games.