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