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
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
- Generalised static checking for type and bounds errors, Stephen Kell, September 2019 -- March 2023, NCSC, £75,000.
- Building Verified Applications in CakeML, Scott Owens, October 2018 - September 2021, NCSC £74,000
- Specification and Verification of C++ Data Structure Libraries, Mark Batty, October 2018 - September 2021, NCSC £82,000
- Verifiably Correct Transactional Memory, Scott Owens and Mark Batty, September 2018 - August 2021, EPSRC £82,900
- Trustworthy Software for Nuclear Arms Control, Aziem Chawdhary and Andy King, May 2018-August 2019, NCSC £72,000
- Compositional, dependency-aware C++ concurrency, Mark Batty, April 2018-March 2020, EPSRC £122,126
- Behavioural API's, Laura Bocchi, March 2018 - April 2022, EC £41,000
- Fast Run-time Verification via Machine Learning, Radu Grigore, January 2018 - December 2019, EPSRC £101,000
- The Rise and Fall of COOP, Andy King, March 2017 - March 2021, GCHQ £121,000
- 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
- Marlowe: Domain-specific language for the design of smart-contracts over cryptocurrencies, Simon Thompson, September 2016 - May 2019, IOHK £207,400
- Vulnerability Discovery using Abduction and Interpolation, Aziem Chawdhary and Andy King, August 2016 – August 2019, 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