Foundations of Computing (FoCo)
We work on a wide range of topics that can broadly be summarised by logic in computer science, and foundations of software science, computer systems and programming languages.
Find out more about Foundations of Computing on our research pages.
Suggested topics
Computer Systems for Reasoning About Binding
Supervisor: Roy Crole
The Hybrid system was developed in Isabelle HOL. It is a metalogic which can be used to reason about languages with binding. One translates the object language into Hybrid, and then uses Hybrid's reasoning principles (such as induction and coinduction) to prove properties of the language. There are a variety of research avenues to explore, ranging from applications of Hybrid which could involve the testing of Hybrid and its comparison with other systems of reasoning with binders, to the further development of the Hybrid system itself.
Mathematical Models of Variable Binding
Supervisor: Roy Crole
In the last decade we have advanced our understanding of the formal notion of variable binding considerably. Presheaf categories have been shown to provide models of standard languages with variable binding, such as (variants of) the lambda calculus, as initial algebras. This is a considerable advancement over older models in which expressions with binders could only be realised as alpha-equivalence classes of elements of initial algebras. The important gain here is the initial algebra gives rise to a clear principle of structural induction. My own work has developed particular kinds of presheaf category models, and a PhD thesis could be based upon the further development of these models and the associated reasoning principles.
The Nominal Lambda Calculus
Supervisor: Roy Crole
The theory of nominal sets has been developed over the past decade as a very general model of variable binding. There are also various kinds of nominal category that provide generalisations of nominal sets. Recent work has been to develop a nominal lambda calculus and a categorical semantics. There are various ways in which these ideas can be further developed, leading to a PhD thesis.
Reversible asynchronous cellular automata
Supervisor: Irek Ulidowski
The aim of this project is to study what reversibility means for different forms of cellular automata, concentrating on asynchronous cellular automata. Examples of problems that can be studied are the universality questions for families of asynchronous cellular automata, both forwards-only and reversible, where we vary how cells are updated, global versus local reversibility, and the time as well as the direction reversibility of asynchronous cellular automata. An integral part of the project will be a development of a software tool for simulation of reversible asynchronous cellular automata.
- Daniel Morrison and Irek Ulidowski, Direction-reversible self-timed cellular automata for Delay-Insensitive circuits. Proceedings, ACRI 2014, LNCS, pp. 367-377. Springer 2014.
- Daniel Morrison and Irek Ulidowski, Arbitration and reversibility of parallel Delay-Insensitive modules. Proceedings, Reversible Computation 2014, LNCS 8507, pp. 67-81. Springer 2014.
- View Irek Ulidowski's webpage and contact details
Reversible debugging of multi-threaded programs
Supervisor: Irek Ulidowski
In the last decade a number of commercial debugging software tools came out that claim to make a full use of reversibility when debugging programs. The most famous example is UndoBD by Undo Software Ltd based in Cambridge, UK.
When it comes to dealing with multi-threaded programs or programs that share memory, these state-of-the-art debuggers use a technique called serialisation, which records a run of a multi-threaded program as a "sequence" of instructions. This removes the information about causality, concurrency and mutual exclusion between instructions in different threads. So, in some sense, reversing a run of a multi-threaded program is reduced to backtracking in a serialised run. In general, it is not clear what is the logically and operationally correct form of reversibility here. The situation is complicated further by various optimisation tasks performed during execution, which effectively change the program order.
This project aims to explore reversibility of multi-threaded programs by taking the formal methods approach. We aim to develop a robust method for reversing simple multi-threaded programs using a process calculus or event structure-like models. The understanding of reversibility of parallel programs for the purpose of debugging must be reached in the setting of the so-called weak memory models, such as, for example the weak memory model of Java. Also, another issue that reversible debugger developers are concerned with, and which we aim to solve in this project, is multi-threaded recording.
Rewriting and Lambda Calculus
Supervisor: Fer-Jan de Vries
We are interested to extend the theory of rewriting with infinite reductions and infinite terms. This leads to new insights when one tries to generalise results and concepts of finite rewriting to the infinite setting.
See papers that I've written with colleagues.
Areas that are waiting to be explored are:
Models for infinitary lambda calculus
The study of infinite lambda calculus has revealed an abundance of different syntactic models. Is it possible to construct models that induce the same equality relations as these syntactic models with other means, for instance via domain equations? The converse question is of interest too: given a known semantics of the lambda calculus, what is the corresponding infinite lambda calculus whose term model induces the same equality relation?
Infinite lambda calculi without renaming
Traditional finite lambda calculi follow a variable convention. Various solutions have been proposed to circumvent this problem: for instance De Bruijn indices or the Adbmal calculus of Hendriks and van Oostrom. Do these solutions generalise?
Weakly orthogonal rewriting
Weakly orthogonal rewriting is confluent in finite rewriting. Does this generalise to infinite rewriting?
Undefined terms
For term rewriting and for lambda calculus there is a notion of meaningless set. Meaningless terms need to be identified in order to regain confluence in the infinite orthogonal setting. Is there a notion of meaningless set for other rewriting formats, like Klop's combinatory reduction systems?
Decreasing diagrams
Decreasing diagrams is a powerful technique to prove confluence in finite rewriting. Can it be generalised to prove confluence in the infinite setting?
Verified filesystem
Supervisor: Tom Ridge
Filesystems are incredibly important, particularly when applications must provide some form of persistence for their data (eg a database must ensure that data survives a complete system failure). In order to develop applications that use the filesystem, one has to know what guarantees are being provided by the filesystem. Unfortunately current filesystems do not provide many guarantees beyond POSIX "atomic move" (if you move a file, and the system crashes, then either the file moved or it did not).
The aim of this project is to develop a filesystem which guarantees certain key properties that application developers depend on. The filesystem will be developed in a functional language such as Haskell, OCaml or SML. Verification will use a theorem prover such as Isabelle, HOL, or Coq. The aim is to develop a reliable filesystem that can be used in real-world systems such as Linux.