Programming Languages and Systems: PhD Studentships
This projects are merely suggestions and illustrate the broad themes of the research group. Potential research students are encouraged and welcome to produce their own suggestions in these research areas or other research areas in the field. All applicants are invited to contact the head of the group, Andy King, if they are considering an application.
Contracts for communicating Erlang processes
Contact: Olaf Chitil
Erlang is a concurrent functional programming language designed by Ericsson with dynamic process creation and asynchronous message passing. The aim of the research project is first to define a language for expressing properties of process creation and communication, for example communication protocols. These properties are expressed as contracts that state which program part to blame if the property does not hold. Contracts shall prevent many concurrency-related runtime errors but still allow common Erlang programming patterns. The second challenge is to devise methods for checking these contracts. Checking could be either statically at compile time or dynamically at run-time. Static 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 project will build on a wide area of previous research on type systems, tracing, dynamic and static contracts for functional languages and session types.
Tracing real-world functional programs
Contact: Olaf Chitil
The Haskell tracer Hat (www.haskell.org/hat) consists of a trace generation system plus various tools for viewing a trace. Hat demonstrated its enormous value for locating faults in Haskell programs. However, it is not used in practice, because its trace generation system only handles Haskell 98, a small subset of the real-world Haskell language compiled by the Glasgow Haskell compiler ghc. Thus the heart of this project is the design and implementation of a local modification of the Glasgow Haskell compiler such that its executables generate traces at run-time. This work will be followed by detailed studies of using traces of real-world Haskell programs. The experience will directly lead to ideas for improvements. For example, it is already clear that for most purpose only the computations of some program parts have to be traced whereas standard libraries and other parts are trusted to be correct and hence are not traced. Although trusting is a well-known concept in tracing, a useful scheme still needs to be developed.
Extending the concept of dependability case to address resilience
Contact: Rogerio de Lemos
A resilient system is a system that is able to deliver service that can justifiably be trusted, when facing changes, in other words, the system has to be dependable when facing changes. Similar to dependability cases, which is based on the concept of safety cases, a resilience case could be seen as a clear and defensible argument that a system is acceptably resilient in a certain operational context. What distinguish the operational context of a dependable system from that of a resilient system are the changes that might occur to the environment of the system, to the system itself and its requirements. The challenge now is how to define a dynamic operational context, instead of a very particular operational context, which has been the basis for producing safety cases. Relying on existing work on dependability and safety cases, the aim of this work is to define what should be a resilient argument, and how a collection of these could be use to build a resilient case.
Dynamic processes for self-adaptive software systems
Contact: Rogerio de Lemos
The self-adaptation of a software system is a complex process that depends on the system requirements, its operational state and environment, which may change during the system operational lifetime. Hence, the process for coordinating the self-adaptation should also be adaptable to changes that may occur during run-time. As a means for coordinating the self-adaptation process of software systems, a solution is to employ workflows that are dynamically generated for dealing with the variability associated with the self-adaptation process. In this context, the aim of the project is to define and develop techniques for automatically generate workflows for coordinating the self-adaptation of software systems.
Garbage collection for very large heaps
Contact: Professor Richard Jones
Despite 50 years of research into automated memory management
(a.k.a. 'garbage collection'),
new applications and new contexts continue to throw up challenges.
One such challenge is posed by very large servers supporting
modern applications such as Twitter, etc. Stopping the world to collect
a heap of tens or hundreds of gigabytes will pause applications
for seconds or several minutes - this is not acceptable.
While it is reasonably straightforward to build a mostly concurrent
collector that does not move objects, this renders large and long running
systems vulnerable to fragmentation.
However, almost all mainstream Java VMs have to stop the world
to compact memory.
In this research project, we will investigate how to manage very large heaps, without fragmentation and without having to stop the world to compact. It is envisioned that the project will encompass a range of techniques including static analysis of Java programs, compiler optimisations and novel garbage collection algorithms.
CRS compilation via nested types
Contact: Stefan Kahrs
Combinatory reduction systems are fairly hard to implement correctly and efficiently, because a simple implementation will be inefficient because it uses repeated renamings of bound variables (de Bruin index adjustments), while an efficient one has a hard task to get the renamings right. However, the de Bruin indices can be expressed through nested types too which would guarantee (a large part) of the correctness of the renaming. The task is to bring these two worlds together.
Implementation of optimal reduction
Contact: Stefan Kahrs
20 years ago Lamping came up with the idea of optimal reduction for the lambda-calculus, supported by a graph-like structure that would make even fewer reductions than lazy evaluation. An implementation as a proof of concept was done in Bologna some years later, but there has been no serious attempts at replacing real-world functional programming implementations with a system based on these ideas.
Algebraic effects for SMT solvers
Contact: Andy King
SMT solvers search for solutions to formulae: they either find an assignment of variables to values that satisfies the formula, or report that no such assignment exists. SMT solvers are complicated to design and implement, hence this PhD project will start by exploring how the control-flow deployed in a SMT solver can be realized using algebraic effects.Algebraic effects provide a clean way of rewinding a call stack on demand (realise exceptions), implement backtracking, restoring a stack at a location, and are now available in C, which suggests they that can be useful in SMT solving.
Reverse engineering tools
Contact: Andy KingReverse Engineering is the process of taking a software artifact, such as a binary, and figuring out what it does. Reversing is important in the security industry where security engineers frequently have to inspect binaries when searching for security holes. This project will develop tooling not for reversing a binary to, say, a C program or even an intermediate language. Rather the project will develop tools that explain what a binary does by annotating it with information that details the values registers and stack slots can potentially store. This will be achieved, not by directly executing the binary (since the binary may be malicious) but rather by following all paths through the binary. The studentship will develop this idea and apply it to develop tools for supporting security engineers.
Inductive programming for better testing
Contact: Professor Simon Thompson
How can you tell how good a set of tests you have? One answer is to look at how much of your program they "cover", or at how they fail when you mutate the program a little. Another approach, which we began to explore in the ProTest project on property-based testing, is whether we can infer a program from the set of tests, and assess whether or not it has similar behaviour to the existing program.
In ProTest we concentrated on state-based systems; in this project the idea would be to look at tests for pure functional programs - written in Haskell - and object-oriented programs - written in Java - and to extract programs from the tests to compare with the originals. More information about the ProTest work can be found here and here.
Refactoring dependently-typed programs
Contact: Professor Simon Thompson
There is a growing interest in dependently-typed functional programming, in systems like Agda as well as in theorem provers such as Coq. In a dependently-type program, the type of the result of a function can depend on the value of a function argument, so that types can give a much closer description of the behaviour of a function, and indeed in the most complex case, represent the full specification of a function.
One of the big problems that emerges in using a dependently-typed system is its sensitivity to the way that data are represented. While abstractly lists of a certain length are equivalent to finite maps of a particular kind, it's often useful to be able to convert between data representations in developing a system. This is a challenging use case for refactoring of such programs, and this thesis project aims to build a tool to support a portfolio of refactorings for dependent types and programs using them.
The Kent functional programming team have world-leading expertise in building the refactoring tools Wrangler for Erlang and HaRe for Haskell; we've also been thinking about dependently-typed programming for twenty years.