School of Computing

Programming Languages and Systems


The Programming Languages and Systems (PLAS) research group researches both practical and theoretical aspects of program design and system building.

Our work in languages encompasses programming across a broad range of paradigms: concurrent, imperative, functional, logic and object-oriented.

These interests are complemented by architectures and systems research in intrusion detection, mobile and distributed systems.

Our work is linked by shared interests in semantics, verification and implementation. Common aspirations of the PLAS group are to develop techniques and tools for program manipulation, ensure program correctness, and improve the reliability and security of programs.


Research Themes

The group focuses on the specification, design and implementation of computer systems, from the very large to the very small, and characterised by the interplay between theory and practice. It has three main research themes: verification and dependability; memory management; and program development.


Verification and dependability

Stefan Kahrs has developed foundational proof techniques for rewriting, which in turn underpin work on program correctness. Eerke Boiten is concerned with the relation between state-based and behavioural specification methods.

Andy King has developed techniques that apply abstraction to automatically diagnose flaws in existing programs. Rogério de Lemos has applied verification at the architectural specification level to assure dependability.

Mark Batty has developed rigorous specifications for the C and C++ memory model and OpenCL. Scott Owens has co-developed a verified implementation of ML. Radu Grigore has developed data-structures for runtime verification.


Memory management

Professor Richard Jones' work has focused on garbage collection on multicore systems, including understanding the overheads placed by concurrent applications on runtime systems, reducing memory overheads in real-time systems, and exploring locality.


Program development

Professor Simon Thompson has developed the Wrangler refactoring tool for Erlang and developed techniques for users to
define new refactorings. Olaf Chitil has explored how contracts - expressing requirements for functional programs - interact with laziness.

Meng Wang has designed languages for bidirectional transformations and property-based testing.

Fred Barnes has shown how to develop concurrent programs that are correct by design. Laura Bocchi has extended session types with logics to enable design by contract for concurrency.


Interested in postgraduate study?

We recruit new PhD and MSc research students every year. We offer a research environment of international quality and an impressive support package for research students.


Currently funded projects

Projects of the research group (see the list on the right for more). A full list of research group projects can be found here.



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

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

Last Updated: 16/09/2016