Preprints
-
Pairwise Coprime Nonrepresentable Integers for Two Coprime Bases
Preprint, 2026Let p > q ≥ 2 be coprime integers. Call a positive integer (p, q)-nonrepresentable if it cannot be written as a sum of terms p^i q^j for which no two distinct terms divide each other. Erdős and Lewin asked for which pairs there is an infinite sequence of pairwise coprime (p, q)-nonrepresentable integers. Yu and Chen answered this question except for the pairs (5, 2), (9, 2), and (5, 3). We prove the remaining cases. The proof works by creating a criterion for generating such sequences, which can then be applied to the three pairs.
Publications
-
Formalising Subject Reduction and Progress for Multiparty Session Processes
ITP, 2025Multiparty 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
Oxford CompSoc, Oxford, UK, 2025-11-23Invited TalkSlidesOn 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
ITP 2025, Reikyavik, Iceland, 2025-09-28Paper PresentationSlidesAs 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
Oxford CompSoc, Oxford, UK, 2025-03-08Invited TalkSlidesAn introduction to the Rocq programming language, as part of a lecture series on programming languages.
-
Subject Reduction for Synchronous MPST in Coq
Department of Computer Science, University of Oxford, Oxford, UK, 2024-11-20Invited TalkSlidesThis 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.