Please feel free to get in touch, if you would like to discuss any of the topics listed below or any other project ideas related to automata, lambda calculi, programming languages or verification. The project topics listed below are not set in stone and can be tailored to individual interests. I have grouped them to indicate (roughly) their relationship to taught courses.
βη-equivalence is the main notion of equivalence studied in courses on the lambda calculus. However, from the point of view of programming languages, another notion of equivalence is more relevant: contextual equivalence. Intuitively, two terms are contextually equivalent if they behave in the same way in any context. The purpose of the project is to design and implement a contextual equivalence checker for the simply-typed lambda calculus by combining ideas from various research papers as well as adding your own.
Enthusiasm for the lambda calculus and strong proof skills are essential.
Two pushdown automata (PDA) are equivalent if they accept the same language. The problem of deciding whether two given PDA are equivalent is known to be undecidable. However, it becomes decidable when the two automata are deterministic. It took 30 years to find an algorithm that, given two deterministic PDA, will be able to determine whether or not they are equivalent. The first one was given in 1997 by Geraud Senizergues, who was subsequently awarded the Goedel Prize for the result. Senizergues' original algorithm has since been considerably simplified by other researchers.
The primary objective of this project will be to understand the latest simplification due to Jancar (cited below) and implement the algorithm in several special cases to understand its complexity. The complexity of the general case is still an open problem, which would be more suitable for a DPhil project.
This is a challenging project focussed on a cutting-edge problem in theoretical computer science. An excellent grasp of automata theory and enthusiasm for exploring the latest techniques in the area are essential.
This project contains solving equations of the form F X = G (for given F, G) with respect to βη-equality. Such equations can be viewed as matching problems (up to βη). In restricted cases (types of low order), it is known how to solve them using tree automata. The purpose of the project is review existing decision procedures for the problem, optimise/simplify them as much as possible, and implement a solver.
Enthusiasm for the lambda calculus and automata.
Logical relations are an established technique for proving properties of lambda terms and, more broadly, programming languages involving higher-order types (not necessarily purely functional). Among others, they can be used to show that the simply-typed lambda calculus is strongly normalising or to support equivalence proofs for programs, such as those needed to validate compiler transformations. Two programs are contextually equivalent if and only if they can be used interchangeably without affecting the result. The aim of the project is to explore the logical relations technique and automate some of its aspects.
This project is related to the lambda calculus and principles of programming languages. It will attempt to transfer techniques from computer-aided formal verification to the setting of higher-order programming languages.
The aim of the project is to understand the state of the art in verifying security protocols, and to try to deploy automata-theoretic methods in the area. Standard automata theory is based on finite alphabets, which is not quite suitable in this context, so the project will explore automata models over infinite alphabets.
Good knowledge of automata theory and a liking for algorithm design.
The Syntactic Control of Interference (SCI) is a typing system for higher-order programs with state that eliminates covert interference by preventing sharing of variables between functions and their arguments. Reasoning about such programs is easier and decidable. The technical goal of the project is to understand how SCI programs are modelled using multi-tape deterministic finite state automata and to identify fragments that can be analyzed in an efficient way, possibly using simpler automata-theoretic formalisms.
Good knowledge of automata theory and a liking for type systems and algorithm design.