School of Computing

Programming Languages and Systems

The Programming Languages and Systems (PLAS) research group researches both practical and theoretical aspects of programming language design and system building. Our work in languages spans programming across a broad range of paradigms including: imperative, object-orientated, functional and logic programming, and even assembler. These interests are complemented by our architectures and systems research in concurrency, relaxed memory, verified compilation and garbage collection. All our work is linked by shared interests in semantics, type systems, verification and implementation.

Mark Batty works on concurrency, software verification, relaxed memory, programming language semantics and GPU concurrency

Laura Bocchi works on automata theory and behavioural types for the verification of concurrent, time-sensitive processes.

Olaf Chitil explores type error debugging and how contracts - expressing requirements for functional programs - interact with laziness.

Radu Grigore is developing refinement techniques for program analyses and works on run-time verification.

Rogério de Lemos applies verification and validation techniques at the architectural level to assure resilience.

Richard Jones focuses on garbage collection on multicore systems studing the overheads placed by concurrent applications by runtime systems.

Stefan Kahrs is developing foundational proof techniques for rewriting, which will underpin work on program correctness.

Stephen Kell is evolving operating systems and language runtimes to make programs more debuggable and interoperable.

Andy King is formalising decompilation and is developing automatic techniques that apply abstraction to automatically diagnose flaws in programs.

Julien Lange applies automata theory and model checking to the implementation and verification of concurrent and distributed systems.

Stefan Marr works on meta-programming, reflection, parallelism and debugging tools.

Matteo Migliavacca works on high-performance event processing in large scale and cloud scenarios.

Dominic Orchard works on type systems and semantics and has developed verification techniques for computational science.

Scott Owens applies interactive theorem proving and is co-developer of CakeML, a verified implementation of ML.

Tomas Petricek works on programming tools for data science; functional programming and considers programming from the philosophical perspective

Simon Thompson devises refactoring tools and is developing domain specific languages for cryptocurrencies.


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.
Our list of PhD projects is merely indicative; we are always interested in projects sugested by students if they overlap with our research interests.

Recent research projects



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

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

Last Updated: 26/02/2019