Programming Languages and Systems
The Programming Languages and Systems (PLAS) research group is actively researching in 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's research is concerned with the relation between state-based and behavioural specification methods. Andy King and Jael Kriener have 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. Funded by NCR, he has applied work on artificial immune systems to anomaly detection in ATMs, leading to the award of patents.
- 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, which is the subject of a REF impact case study. His team has also demonstrated how to verify the correctness of refactorings, and developed techniques for users to define new refactorings. Olaf Chitil has explored how contracts - expressing requirements for functional programs - interact with laziness. Professor Peter Welch and Fred Barnes have shown how to develop concurrent programs that are correct by design. Their work is applicable both to programs written in conventional parallel languages and those coded in occam-pi, of which Peter Welch and Fred Barnes are the principal architects. This is the subject of another impact case study.
The Programming Languages and Systems Group will consolidate recent staff appointments and funding success in both verification and concurrency. The overall aim will be to sustain impact by working with government agencies and industrial organisations, and releasing research results as open source systems. The group will also set the goal of publishing in the most prestigious venues, as well as ensuring the widest visibility for its results. Our future research focus will be:
- To investigate how concurrent languages can be extended to better support correctness-by-design, and explore how to systematically verify compilation.
- To investigate memory management for many-core and other emerging computer architectures; and low-energy virtual machines.
- Through underpinning foundational work in the semantics of rewriting systems, functional programs and binary programs, the group will develop novel semantically-based tools for program development, refactoring, tracing and security fault diagnosis.
- To leverage mechanical verification technology to justify refactorings, program analyses and end-to-end compilation.
- To devise fault-tolerant architectures for dependable systems.
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.
Interested in postgraduate study?
We are recruiting new PhD and MSc research students to these research projects and others. We offer a research environment of international quality and an impressive support package for research students.
Research in the group is supported by the following organisations: