Theoretical Computer Science Research Group

List of Possible Research Projects

These projects are only suggestions and examples of areas that the research group is interested in, and not all members of staff who are interested in supervising students are listed. Potential research students are encouraged and welcome to produce their own suggestions in these research areas or other research areas in the field. Moreover, it is unlikely that a research project will remain fixed throughout the lifetime of a studentship as students develop a greater appreciation of the subareas that are of most interest to them.

Please email Andy King, the Head of the Research Group, telephone 01227 827694 or visit the group home page http://www.cs.kent.ac.uk/research/groups/tcs/ for further information

Discovering Invariants by Solving Constraints
One of the best ways to understand a program is to figure out what invariants hold; any program that, on completion, puts an array of numbers into ascending order we would instantly recognise as a sort. Invariants also help us to argue that things to do not go wrong, for example, that an array is always indexed in range or that a loop always terminates.  Therefore there has been much interest in automatically discovering invariants. Recently it has been shown how (Boolean) constraint solving can be applied to this problem.  The idea is to encode the paths through a program as Boolean constraints, and then repeatedly solve the constraints, so as to enumerate different paths. By confining the invariants to certain classes, it is possible to summarise all paths in a finite number of steps, and hence derive an invariant.  It has been shown how this technique enables efficient (Boolean) constraint solvers to be applied to discover invariants that cannot be found by other methods. However, there is no reason why this technique cannot be refined to derive richer invariants by applying different constraint solvers.  The PhD studentship will explore this promising thread of work.
Contact: Andy King	Email: amk@kent.ac.uk
Reasoning About Scratch Cards
Scratch cards are used widely in lotteries and games, and recently also in e-voting protocols. However, public confidence in e-voting is very low. This project will develop mathematical and logical abstractions of scratch cards that allow formal reasoning, and consequently watertight proofs of the security.
Contact: Eerke Boiten	Email: eab2@kent.ac.uk
Static Contracts for Communicating Erlang Processes
Erlang is a concurrent functional programming language designed by Ericsson with dynamic process creation and asynchronous message passing. Type systems have been defined on top of the dynamically typed Erlang language, but these concentrate on the traditional, non-concurrent aspects of the language. The aim of the project is first to define a language for expressing properties (i.e. contracts) of process creation and communication, for example communication protocols. These contracts shall prevent many concurrency-related runtime errors but still allow common Erlang programming patterns. The second challenge is to devise algorithms for statically checking these contracts. The project will build on a wide area of previous research on type systems, dynamic and static contracts for functional languages and session types.
Contact: Olaf Chitil	Email: oc@kent.ac.uk
Tracing Functional Programs with Hat
Hat (www.haskell.org/hat) is a sophisticated tool for locating faults in Haskell programs. Hat consists of a trace generation system plus various tools for viewing a trace. The aim of the research project is to improve Hat by both extending it and easing its application in practise: (1) Integrate the trace generator of Hat into the byte code interpreter of the Glasgow Haskell system (GHC). (2) Enable traced code to call and be called from unmodified non-tracing code, such that Hat can use pre-compiled libraries of GHC. (3) Apply several theoretical results of a recent EPSRC project on tracing in Hat (e.g. algorithmic debugging with functions as finite maps). (4) Develop and implement new ways of displaying computations of common programming patterns, for example for the IO monad and monads in general.
Contact: Olaf Chitil	Email: oc@kent.ac.uk
Productivity Proofs for Functional Programs
Related to the halting problem, lazy functional programming has the issue whether program that potentially produce an infinite amount of data are 'productive', i.e. whether they keep producing data in case they fail to terminate. For (higher-order) functions a form of hereditary productivity is required: functions need to be productive themselves but should also map productive computations to productive computations. The aim of the project is to (i) study the theoretical foundations of these properties, and (ii) based on those foundations, build a tool that is capable of certifying programs as productive or warn about program parts whose productivity is questionable.
Contact: Stefan Kahrs	Email: smk@kent.ac.uk
Convergence Proofs for Infinitary Term Rewriting
In infinitary term rewriting, evaluations may not terminate after finitely many steps but instead still produce a sensible outcome by converging to a result in the limit. Moreover, we say that a rewrite system is convergent if all its reduction sequence converge - in analogy to calling rewrite systems terminating if all their reduction sequence terminate.  The aim of the project is to come up with new and automatisable ways of proving convergence.
Contact: Stefan Kahrs	Email: smk@kent.ac.uk
How Do Students learn Haskell?
As users and teachers of Haskell, we have some sense of how people, both experienced programmers and novices, learn to program in Haskell. This sense is based on experience - as learners ourselves, perhaps, or through teaching. We propose an alternative approach, based on the wealth of data collected through the instrumented version of the Helium system for Haskell.  This collects information of the programs compiled, the errors they generate, and how learners use the system in fixing those errors, and so we can see precisely the way that learners use these tools while they are learning. This is a joint project of the Functional Programming and Computing Education groups at the University of Kent, and the Helium group at Utrecht. The CompEd group has experience of working on this sort of project, and the FP group has wide experience of teaching functional languages, particularly Haskell.
Contact: Simon Thompson and Sally Fincher	Email saf@kent.ac.uk: sjt@kent.ac.uk