School of Computing

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 academic associated with the project when making an application.

Mathematical specification of C++ concurrency libraries

Contact: Mary Batty

We write rigorous mathematical specifications of messy real-world parts of the computer system, providing a formal basis for reasoning about code, and helping to improve the official definitions of the system. Our fixes for flaws in the low-level concurrency specifications of C and C++ have been adopted by the International Standards Organisation (ISO). We have shown that fundamental flaws remain, but we have a new definition that fixes these. The ISO are developing definitions of higher-level concurrency libraries, e.g. distributed counters and concurrent queues. This project will build mathematical specifications of the new C++ library definitions, incorporate them into our mathematical formalism, and validate implementations of the library either using mathematical proof or automated solvers. This is an ambitious theoretical project with the potential for real-world impact. It will involve developing skills in formal specification, mechanised theorem proving (e.g. HOL, Coq, Isabelle), and the use of automated solvers (e.g. QBF).

Behavioural APIs for robust communicating systems

Contact: Laura Bocchi

In this project you will develop a theory and tool for design and implementation of robust communicating systems. The project will centre on Behavioural APIs. Behavioural APIs are abstract specifications of application-level protocols; they go beyond traditional APIs in that they specify conversation patterns among components/services (and not just sets of supported operations). Behavioural API have been successfully applied to guarantee safety (e.g., absence of deadlocks) via code generation, verification and monitoring. The project will focus on extending known techniques by gradually dropping ideal-world assumptions and handling unexpected scenarios (like unexpected delays and failures).

From correct real-time models to correct real-time programs

Contact: Laura Bocchi

Verification of real-time models (e.g., timed automata) is supported by well-established theories and tools. Once a real-time model is proved correct, one must make sure that correctness properties do not “get lost in implementation” (i.e., that the implementation of the model preserves its desirable properties). In this project you will develop a formally grounded framework that supports development of correct programs out of correct models. You will work on automata theory (e.g., on novel notions of refinement), programming languages (e.g., on mapping models into APIs for some language, such as Erlang, Go, or Java), and tool development.

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 ( 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.

Fast Runtime Verification

Contact: Radu Grigore

Tools like ThreadSanitizer monitor running programs for data races. Valgrind is a framework for building monitors that detect other types of errors. For example, there exist tools based on Valgrind that detect memory management errors. Such tools are indispensable during development. But, they have two drawbacks: (1) their overhead is prohibitive, and (2) they cannot be used for finding higher-level errors. To see why big overheads are a problem, consider ThreadSanitizer: it makes programs run 10 times slower. Clearly, ThreadSanitizer cannot be used to find errors in production code. To see why detecting higher-level errors would be desirable, consider the well-known fact that data-race free programs may still be incorrect. In this project, you will tackle these two problems: (1) How to reduce the overhead of runtime monitoring? (2) How to monitor for higher-level errors, specified by developers?

Program Analysis for Speed

Contact: Radu Grigore

The theory of computer science looks at two main aspects of algorithms: their correctness and their efficiency. Program analysis tools are traditionally used to help ensure program correctness. In this project, we will look at the following research question: How can program analysis be used to ensure program efficiency?

Garbage collection for very large heaps

Contact: 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.

Coalgebraic invariant verification

Contact: Stefan Kahrs

Certain invariants of rewrite systems, functional programs and the like can be proven by verifying them for (all) finite coalgebras. This requires an induction over finite coalgebras which is very tedious by hand - therefore the aim is to push this into theorem provers/checkers such as Isabelle or Coq.

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 King

Reverse 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.

Choreography-driven verification of message-passing programs

Contact: Julien Lange

Message-passing based concurrency is getting more popular thanks to the rise of programming languages such as Go and Rust. These concurrent programs are currently no easier to verify and debug than any other concurrent programs based on, e.g., shared memory, but that need not be the case. The idea of this project is to apply theories based on behavioural types, communicating automata, and choreography synthesis to design theories and/or tools that will help developers verify and debug their message-passing programs by manipulating an easy-to-work with bird's-eye view of their program.

Program optimisation through protocol optimisation

Contact: Julien Lange

Today's distributed systems rely on many different communication technologies and associated standards, e.g., AMQP, STOMP, etc. Each of these can be used and tweaked differently to attain specific goals. The common denominator is that all allow programs to exchange messages which travel on the network according to different policies. The order in which these messages are sent and received can be described as a protocol, which specify precisely the structure of communications between programs (using, e.g., communicating automata or session types). The idea of this project is to apply different optimising strategies to these protocols so that, depending on the messaging technology used, the overall behaviour of the distributed systems perform faster. The challenge is to get better performance while preserving the safety properties of the original protocol.

Reconciling blocking and nonblocking concurrency abstractions

Contact: Stefan Marr

Blocking concurrency abstractions such as locks, channels, and join operations are designed to ensure deterministic execution. However, their blocking semantics are inherently incompatible with nonblocking programming models such as the communicating event loop model. In such nonblocking models, the benefits of asynchronicity are easily leveraged, but developers need to work around the lack of determinism explicitly. The goal of this project to extend the versatility of blocking and non-blocking programming models by introducing new programming abstractions, without weakening the inherent guarantees of either kind of model. A first task in that direct will be to identify underlying principles of blocking and nonblocking abstractions and the use cases they enable.

Building blocks for dynamic languages with state-of-the-art performance

Contact: Stefan Marr

Dynamic language implementations share many concepts and features, but share rarely implementations. With the Truffle/Graal platform, we get state-of-the-art performance by reusing the existing just-in-time compiler, garbage collectors, memory models, and threading system. However, there is still much duplication of effort to realize basic operations, control-flow structures, AST-level optimizations, debugger support, or concurrency abstractions. While some of is is justified by language differences, there remains a large potential for reuse to simplify language implementation and design exploration. The goal of this project is to identify and design reusable components that provide sufficient flexibility to account for language differences, while enabling reuse and state-of-the-art performance.

Multi-stage semantics and typing via graded modalities

Contact: Dominic Orchard

Staged computation (otherwise known as meta programming) is a powerful technique for writing programs that generate programs. This might be in a simple macro language, or a more involved compile-time code generator, or even a multi-stage pipeline of multiple languages or sublanguages, including JIT. It turns out that intuitionistic modal S4 logic generates a useful type system for staged computations (through a Curry-Howard like isomorphism), detailed in the work of Davies and Pfenning (A modal analysis of staged computation, 2001). The aim of this project is to generalise their approach to graded modalities, capturing truly multi-stage programs: not just 2 stages, but n-stages, with their interactions controlled and described by a graded modal type system. This approach can then be combined with other kinds of graded modality to explain the role of data across multiple levels of a staged compilation pipeline.

Program synthesis from type-based resource-sensitive specifications

Contact: Dominic Orchard

Type systems are one of the most widely deployed verification techniques in programming today. Type systems offer a simple "first defense" against a range of programming mistakes, directly within a language. Since types provide partial specifications of program behaviour, it is sometimes possible to use a type specification (a type signature) to derive parts of a program automatically (program synthesis) therefore speeding up programming. Type-based program synthesis is especially powerful in the context of more advance type theories, such as dependent types, where the synthesis amounts to proof search in logic. Various languages such as Agda and Idris now provide interactive modes where the human and the computer work together to write a program, with a programmer writing a specification and the compiler synthesising as much of a candidate program as possible, and so on. The aim of this project is to take program synthesis to the next level by combining dependent types with linear and graded types. Linear and graded types provide mechanisms for explaining where and how data is used, allowing a view of data as a resource with possible constraints attached. Linear and graded types further restrict the set of possible programs and thus offer a way to improve program synthesis by further constraining a program via "resource sensitive" types. This project will develop both the theory and practice, with a chance to implement the program synthesis / proof search techniques on top of the state-of-the-art language Granule.

The Plastic programming language

Contact: Simon Thompson

The aim of this project is to design and prototype a “plastic” programming language in which programs can be moulded into shape to work most effectively and efficiently. This means getting away from a textual representation of the program, instead allowing us to build programs up as a series of small steps, that can be combined and reconfigured. In practice we will build programs as trees (with extra information), into a git-like repository for this kind of structure, with operations to reflect program construction and refactoring.

Refactoring dependently-typed programs

Contact: 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.



School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 22/01/2019