One of my co-authors, Jamie Wright, will be presenting the paper at @etapsconf.bsky.social later today!

Rely-Guarantee Is Coinductive We make the case that the foundation for Rely-Guarantee reasoning can be fruitfully delivered by a coinductive semantics. Using insight from an Isabelle formalization, via a proof analysis we show tha...

Another paper from my postdoc is available! "Rely-Guarantee is Coinductive" explores a proof-centered investigation of Inductively Approximated Coinduction and RG definitions, and was accepted to ESOP2026. link.springer.com/chapter/10.1...

Workshop link here: aitpm.github.io

Looking forward to participating and speaking at an online workshop on ITPs and AI in mathematics over the next few days! Thanks @adbrucker.bsky.social for the invitation to speak and to the organising team at Exeter University for making it possible to participate from anywhere in the world.

CICM (Conference on Intelligent Computer Mathematics) was where I first published a paper, so it is exciting to be on the PC for this year's conference in Slovenia in September! The Call for Papers is now online (cicm-conference.org/2026/cicm.ph...), Abstracts due March 25.

It was great to be a lecturer at the #ANU #LSS (Logic Summer School) last week! I taught a course on "Proof Engineering for Program Logic in Isabelle/HOL", resources available here: cledmonds.github.io/anulss2025/

Model Checking Buffered Durable Linearizability in CSP Non-volatile memory (NVM) is a high-performance memory technology that supports persistency (i.e., durability) of data in case of a system crash (e.g., power failure). For implementations of concurren...

iFM paper: link.springer.com/chapter/10.1...

Relative Security: (Dis)Proving Resilience Against Semantic Optimization Vulnerabilities in Isabelle/HOL - Journal of Automated Reasoning Meltdown and Spectre are vulnerabilities known as transient execution vulnerabilities, where an attacker exploits speculative execution (a semantic optimization present in most modern processors) to b...

JAR Paper: www.doi.org/10.1007/s108...

Last week not one but two papers were published from my postdoc! At iFM2025 a paper on model checking buffered durable linearizability, and in the Journal of Automated reasoning an extended paper on relative security for reasoning on spectre-like vulnerabilities in Isabelle/HOL. Links in comments.

Any chance I could be added to this list? Just moved back to Australia - now based at UWA!

Exploring campus after my first day as a Lecturer at UWA today. Pretty nice view to end a work day!

I’m excited to share I’ll be starting as a Lecturer (equiv. Assistant Professor) at the University of Western Australia this November. Keen to start (re)connecting with colleagues in Australia while also making the most of my last month in the UK!

It was fun learning about the cool projects in Formal maths happening in Heidelberg too! See here for more details on the seminar series: matematiflo.github.io/FormalMathSe... Thanks to Florent and Judith for the invitation to talk!

It was great to be invited to visit the Mathematikon @uniheidelberg.bsky.social earlier this week to talk about formal maths in Isabelle and my past PhD work as part of their research seminar series on formal mathematics! #postdoclife #IsabelleHOL #FormalMaths

Registration for this closes on Monday the 17th of March!

Great to be a part of this programme this year - thanks to @whiteroseuc.bsky.social for hosting! Really enjoyed connecting with other postdocs across Leeds, Sheffield, and York at the first workshop last week, and looking forward to the next two workshops over the coming months.

Please add me!

16th International Conference on Interactive Theorem Proving - ITP'25

Reykjavik, Iceland, 27 September-3 October 2025

Second call for papers

The ITP conference series is concerned with all aspects of interactive
theorem proving [...] icetcs.github.io/frocos-itp-t...

I'm excited to be one of the lecturers for this year's Midlands Graduate School (MGS) in Sheffield! MGS is primarily for first and second year PhD students in Computer Science Foundations, but is open to anyone interested in the topics. More details are available here: tinyurl.com/MGS-2025