Centre for Programming Languages and Systems
The Programming Languages and Systems group is interested in the expression, meaning, and formal analysis of computational systems. Our goal is the development of robust, secure, and reliable computing systems.
About
At their heart, algorithms maintain a structured state that is updated using mechanical rules. The state can be represented by complex and unbounded internal structures and/or be distributed across a network of communicating nodes. The rules are typically described using programming languages, which need to allow complex algorithms to be succinctly explained, be well-defined in their semantics, and be interpretable by a machine.
While complex behaviours can often be elegantly explained by simple programs, the behaviours of complex programs -- implementing critical real-world tasks -- can be very difficult to predict. Our research tackles the dual aims of programming language design and the formal analysis of the resulting systems, with the goal of developing robust, secure, and reliable computing systems.
Research
Computer Language Design and Analysis and Compiler Construction
Our aim is to enhance research in, and facilitate the application of, software technologies that employ grammar-based techniques and related rewriting systems including Structural Operational Semantics. The work centres on the formal properties and utility of generalised parsing techniques coupled with formal semantic specification and efficient interpretation.
Topics include:
- correct, efficient algorithms for parsing general context free languages,
- Domain Specific Language development,
- reverse compilation,
- the semi-automatic derivation of customised computer architectures for embedded systems.
For more information see here.
Our interest in language engineering also has an historical perspective: we are investigating the formal notations Charles Babbage developed to design and specify his 19th century computing engines: this work led to the construction of a difference engine that is driven by a steam engine, realising Babbage's desire for computations to be able to be performed by steam.
Formal Methods
We focus on formal methods and programming language semantics for classes of real-world systems, including concurrent/distributed, and infinite-state systems. Topics include
- automata theory, including pushdown, register, and communicating automata,
- the use of artificial intelligence in automated verification,
- constraint solving for symbolic execution,
- logic and proof theory,
- type theory and process calculi.
Reliable and Secure Data Management
We study programming principles and paradigms for building robust and secure distributed systems and databases. This research is conducted in collaboration with the department's Distributed and Global Computing Group and with the Software and Systems Security Lab (S3 Lab) of Royal Holloway's Information Security Group. Ongoing work addresses systems challenges arising in cloud and edge computing.
Topics include,
- trustworthy cloud computing (e.g. Intel SGX),
- high performance stream processing,
- edge computing for the Internet of Things,
- information flow control for cloud computing and web applications,
- blockchain and smart contract security.
Members
Core Academic Staff
Research Staff and Students
| Luke Bessant (MRes) |
| Alejandro Flores-Lamas (real-world regular expressions) |
| Thomas Neele (CLeVer project) |
| Stefan Zetszche (PhD student based at UCL) |
| Nicolas Dilley (PhD student based at Kent) |
| Jordy Gennissen (PhD Student, RHUL CDT in CyberSecurity) |
| Alpesh Bhudia (PhD Student, RHUL CDT in CyberSecurity) |
| Nathan Rutherford (PhD Student, RHUL CDT in CyberSecurity) |
Visiting Academics
| Prof. Mark van den Brand, Professor Software Engineering and Technology, Eindhoven University of Technology |
| Prof. Peter Mosses, Delft University of Technology, Professor Emeritus, Swansea University, Honorary Research Fellow |
| Dr Doran Swade, Former curator at the London Science Museum and the Computer History Museum, Silicon Valley. |
Publications
- Multiple lexicalisations (a Java based case study). E.Scott and A.Johnstone, Proceedings of Software Language Engineering, 2019, ACM, 2019.
- GLL syntax for EBNF grammars. E.Scott and A.Johnstone, Science of Computer Programming, 166, 2018.
- Symbolic Register Automata. L. D'Antoni, T. Ferreira, M. Sammartino, A. Silva. CAV (1) 2019: 3-21.
- Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations. T. Chen, M. Hague, A. W. Lin, P. Ruemmer, Z. Wu. POPL, 2019.
- Cyclic Program Synthesis. S. Itzhaky, H. Peleg, N. Polikarpova, R. Rowe, I. Sergey. PLDI, 2021.
- Featherweight Go. R. Griesemer, R. Hu, W. Kokke, J. Lange, I. L. Taylor, B. Toninho, P. Wadler, N. Yoshida. Proc. ACM Program. Lang. 4(OOPSLA): 149:1-149:29 (2020).
- Spons & Shields: Practical Isolation for Trusted Execution, V.A. Sartakov, D. O'Keeffe, D. Eyers, L. Villanova, and P. Pietzuch, VEE 2021.
- Glamdring: Automatic Application Partitioning for Intel SGX, J.Lind, C. Priebe, D. Muthukumuran, D. O'Keeffe, P-L. Aublin, F. Kelbert, T. Reiher, D. Goltzche, D. Eyers, R. Kapitza, C. Fetzer and P. Pietzuch, USENIX ATC 2017
