CV

Current position

• Lecturer, Department of Computer Science, Royal Holloway, University of London

Previous positions

• Lecturer (Assistant Professor), School of Computing, University of Kent, 2021–
• Research Associate, Imperial College London, Mobility Reading Group

Education

• Ph.D. in Computer Science, University of St Andrews, 2018. Thesis: Structured arrows: a type-based framework for structured parallelism

Software

• rocq-hylomorphisms: axiom-free hylomorphisms in Rocq, with idiomatic code extraction (ITP 2025)
• Zooid: certified multiparty session types and processes in Coq (PLDI 2021)
• GoScr: Go code generation for dynamically updatable multiparty session protocols, with benchmarks (ECOOP 2023)

Publications

A Synthetic Reconstruction of Multiparty Session Types

Program Optimisations via Hylomorphisms for Extraction of Executable Code

The Concurrent Calculi Formalisation Benchmark

Dynamically Updatable Multiparty Session Protocols: Generating Concurrent Go Code from Unbounded Protocols

Zooid: a DSL for certified multiparty computation: from mechanised metatheory to certified multiparty processes

EMTST: Engineering the Meta-theory of Session Types

CAMP: cost-aware multiparty session protocols

Compiling first-order functions to session-typed parallel code

Distributed programming using role-parametric session types in go: statically-typed endpoint APIs for dynamically-instantiated communication structures

Automatically deriving cost models for structured parallel processes using hylomorphisms

Structured arrows : a type-based framework for structured parallelism

Farms, pipes, streams and reforestation: reasoning about structured parallel processes using types and hylomorphisms

Towards semi-automatic data-type translation for parallelism in Erlang

Compiling CAO: From Cryptographic Specifications to C Implementations

A Case Study on Verifying a Supervisor Component Using McErlang

Talks

Program Calculation with Hylomorphisms in Rocq

Upcoming

at Seminar,

Calculating Correct and Efficient Programs in Rocq

Upcoming

at Seminar,

A Synthetic Reconstruction of Multiparty Session Types

January 19, 2026

at PLAS Group Talk @ University of Kent,

Towards A Synthetic Formulation of Multiparty Session Types

December 10, 2024

at PLAS Group Talk @ University of Kent,

Mechanising Recursion Schemes with Magic-Free Coq Extraction

May 02, 2024

at Online Seminar @ Tallinn University,

Mechanising Recursion Schemes with Magic-Free Coq Extraction

April 08, 2024

at PLAS Seminar @ University of Kent,

Teaching