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.
Stefan Kahrs is developing foundational proof techniques for rewriting, which will underpin work on program correctness.
Radu Grigore is developing refinement techniques for program analyses and works on run-time verification.
Andy King is formalising decompilation and is developing automatic techniques that apply abstraction to automatically diagnose flaws in programs.
Rogério de Lemos applies verification and validation techniques at the architectural level to assure resilience.
Mark Batty is developing rigorous specifications and tooling for the C and C++ memory model and OpenCL.
Scott Owens applies interactive theorem proving and is co-developer of CakeML, a verified implementation of ML.
Simon Thompson devises refactoring tools and is developing domain specific languages for cryptocurrencies.
Dominic Orchard works on type systems and semantics and has developed verification techniques for computational science.
Olaf Chitil explores type error debugging and how contracts - expressing requirements for functional programs - interact with laziness.
Laura Bocchi works with session types to enable design by contractfor concurrency.
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.
Richard Jones focuses on garbage collection on multicore systems studing the overheads placed by concurrent applications by runtime systems.
Matteo Migliavacca works on high-performance event processing in large scale and cloud scenarios.
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
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
- Compositional, dependency-aware C++ concurrency, Mark Batty, January 2018-December 2019, EPSRC £122,126
- Time-sensitive protocol design and implementation, Laura Bocchi,
December 2016-November 2018, EPSRC, £101,196
- Trustworthy refactoring, Simon Thompson and Scott Owens, September 2016—March 2020, EPSRC £728,766
- Vulnerability Discovery using Abduction and Interpolation, Andy King and Aziem Chawdhary (Research Co-Investigator), August 2016 – March 2018, EPSRC, £199,130
- Testing Techniques for Functional Programming Languages, Meng Wang, March 2016-Feb 2018, Royal Society International Exchange, £10,000
- CGrail: unified, optimisable and formally specified C concurrency, Mark Batty, Jan 2016-December 2020, REng Research Fellowship, £526,646
- Heterogeneous memory model study, Mark Batty, December 2015-March 2016, GCHQ, £19,600
- CamFort: Automated evolution and verification of computational science models, Dominic Orchard (Co-investigator), July 2015-August 2018, EPSRC, £20,000
- Verifying current algorithms on Weak Memory Models, Scott Owens, May 2015-October 2018, EPSRC, £285,988
- Relaxed Memory Model Design for Theory and Practice, Scott Owens, Jan 2014-Jan 2016, EPSRC, £98,538
- Se-Ma-Match: Semantic Malware Matching, Andy King, October 2013-October 2016, EPSRC, £245,525
- Compositional Security Analysis for Binaries, Andy King, August 2013-September 2017, EPSRC, £228,823
- RELEASE: A High-Level Paradigm for Reliable Large-scale Server Software,
October 2011-September 2014, Simon Thompson, EU STREP, £310,000