Publications
-
Multiparty session types (MPST) provide a robust typing discipline for specifying and verifying communication protocols in concurrent and distributed systems involving multiple participants. This work formalises the non-stuck theorem for synchronous MPST in the Coq proof assistant, ensuring that well-typed communications never get stuck. We present a fully mechanised proof of the theorem, where recursive type unfoldings are modelled as infinite trees, leveraging coinductive reasoning. This marks the first formal proof to incorporate precise subtyping, aiming to extend the typability of processes thus precision of the type system. The proof is grounded in fundamental properties such as subject reduction and progress. ...
Talks & Presentations
-
"By Chain Completeness"...? Proofs on Infinite Lists
On a proof scheme as to how we can prove predicates on infinite lists. The scheme itself is introduced to students in Year 1, but this talk covers why the scheme actually works. -
Formalising Subject Reduction and Progress for Multiparty Session Processes
As part of the Interactive Theorem Proving 2025 conference. Copresented, where I talked about the technical mechanization aspects and design choices. -
Introduction to the Rocq Programming Language
An introduction to the Rocq programming language, as part of a lecture series on programming languages. -
Subject Reduction for Synchronous MPST in Coq
This was the final Lecture of Master's Course in Distributed Processes, Types and Programming at the University of Oxford, presenting my work on mechanising subject reduction for synchronous MPST in Coq. This corresponds to the ITP'25 paper.