Skip to main content

Centre for Programming Languages and Systems

Centre for Programming Languages and Systems

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.

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. 

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,
  • formal verification: formalisation of mathematics using interactive theorem provers (proof assistants).
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 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 architectures (e.g. Intel SGX), 
  • high performance stream processing and durable execution, 
  • program analysis for cloud computing and web applications security, 
  • blockchain and smart contract security. 

Core Academic Staff

Research Staff and Students

Chris Purdy (PhD student)
Thomas Neele (CLeVer project)
Sergey Egorov (Post-Doctoral Researcher, Redonda project)
Stefan Zetszche (PhD student based at UCL)
Nathan Rutherford (PhD Student, RHUL CDT in CyberSecurity)
Oliver Pearce (PhD Student, RHUL CDT in CyberSecurity)
Cameron Jones (PhD Student, RHUL CDT in CyberSecurity)
Connor Pfreundschuh (PhD Student, RHUL CDT in CyberSecurity)
Alexis Butler (PhD Student, RHUL CDT in CyberSecurity)
Giuseppe Raffa (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 Doron Swade, Former curator at the London Science Museum and the Computer History Museum, Silicon Valley.
  • Georgian-Vlad Saioc, Julien Lange, and Anders Møller. 2024. Automated Verification of Parametric Channel-Based Process Communication. Proc. ACM Program. Lang. 8, OOPSLA2, Article 344 (October 2024), 27 pages. https://doi.org/10.1145/3689784. 
  • Dennis Liew, Tiago Cogumbreiro, and Julien Lange. 2024. Sound and Partially-Complete Static Analysis of Data-Races in GPU Programs. Proc. ACM Program. Lang. 8, OOPSLA2, Article 357 (October 2024), 28 pages. https://doi.org/10.1145/3689797. 
  • Liron Cohen, Adham Jabarin, Andrei Popescu, Reuben N. S. Rowe: The Complex(ity) Landscape of Checking Infinite Descent. Proc. ACM Program. Lang. 8(POPL): 1352-1384 (2024)
  • Cohen, L., Rowe, R.N.S., Shaked, M. (2025). Cyclone: A Heterogeneous Tool for Verifying Infinite Descent. In: Gurfinkel, A., Heule, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2025. Lecture Notes in Computer Science, vol 15696. Springer, Cham. https://doi.org/10.1007/978-3-031-90643-5_18
  • Koutsoukou-Argyraki, A. and Wapniarski, K.,  A Formalisation of Aristotle’s Assertoric Syllogistic in Isabelle/HOL. Topoi (2025). Springer https://doi.org/10.1007/s11245-025-10184-6
  • Koutsoukou-Argyraki, A., & Paulson, L. C. (2025). Transitive Union-Closed Families (Formal proof development). Archive of Formal Proofs. https://www.isa-afp.org/entries/Transitive_Union_Closed_Families.html
  • Koutsoukou-Argyraki, A. (2024). Wooley's Discrete Inequality (Formal proof development). Archive of Formal Proofs. https://www.isa-afp.org/entries/Wooley_Elementary_Discrete_Inequality.html
  • Scott, Elizabeth ; Johnstone, Adrian ; Walsh, Robert Michael. / Multiple input parsing and lexical analysis. In: ACM Transactions on Programming Languages and Systems. 2023
  • Johnstone, Adrian. / A Reference GLL Implementation. Proceedings of the 16th ACM SIGPLAN International Conference on Software Language Engineering (SLE ’23), October 23–24, 2023, Cascais, Portugal. ACM, 2023. pp. 43-55
  • 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.
  • Solving String Constraints With Regex-Dependent Functions Through Transducers With Priorities And Variables, T. Chen, A. Flores Lamas, M. Hague, Z. Han, D. Hu, S. Kan, A. Lin, P. Ruemmer, Z. Wu, POPL 2022.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).
  • Mangosteen: Fast Transparent Durability for Linearizable Applications using NVM, S. Egorov, G. Chockler, B. Dongol, D. O’Keeffe and S. Keshavarzi. USENIX ATC 2024
  • Revoke: Mitigating Ransomware Attacks against Ethereum Validators, A. Bhudia, D. O’Keeffe and D. Hurley-Smith, ESORICS 2024
  • CloudFlow: Identifying Security-Sensitive DataFlows in Serverless Applications, G. Raffa, J. Blasco-Alis, D. O’Keeffe, S. Kumar-Dash, USENIX Security 2025

Explore Royal Holloway