Chelsea L. Edmonds

Department of Computer Science and Software Engineering

University of Western Australia

Crawley WA 6009

Welcome! I’m Chelsea, a Lecturer (equiv. US Assistant Professor) in Computer Science and Software Engineering at the University of Western Australia. My primary research interests are formalised mathematics, interactive proof assistants such as Isabelle/HOL and Lean, modular formal proof techniques, and formal methods for security and concurrency. I’m also interested in exploring new ideas at the intersection of formal methods, HCI, and computing education.

Previously, I was a Postdoc at the University of Sheffield working on the COVERT project with Dr. Andrei Popescu and Prof. John Derrick (as well as collaborators at Surrey and Kent) – which aimed to develop verification tools and models for reasoning on the security of programs running on advanced architectures. I was awarded my PhD from the University of Cambridge in 2024, which explored how we can develop modular, flexible, and extensible libraries for combinatorial mathematics in Isabelle/HOL, supervised by Prof. Lawrence C. Paulson. I’m grateful to have been fully funded by a Cambridge Australia Scholarship and a studentship from the Department of Computer Science. My PhD work was further acknowledged by a British Federation of Women Graduates Academic Award, and a Distinguished Paper at CPP 2024.

Beyond my research, I’m a passionate educator and an Associate Fellow with AdvanceHE. I’ve been involved in numerous STEM outreach events and organisations, as well as gender diversity initiatives for Women in STEM.

Recent News

Nov 10, 2025	I’m on the review committee for PLDI 2026. The conference will be in Colorado from the 15th to 19th of June and the final call for papers is on the conference website.
Nov 03, 2025	I’ve started my new position as a Lecturer in the Department of Computer Science and Software Engineering at the University of Western Australia! My new work web page and contact details are available here.
Oct 03, 2025	Today was my last day as a postdoc at the University of Sheffield. Thank you to all my friends and colleagues in the Sheffield Department of Computer Science for their support over the last two years!
Sep 15, 2025	I’ve accepted a continuing position as a Lecturer (equiv. Assistant Professor) at the University of Western Australia, and will be starting in November. Very excited to be moving home to Australia after 6 incredible years in the UK, and thankful to all those who supported me to get here!
Sep 01, 2025	I’m looking forward to being a lecturer at the ANU Logic Summer School in December this year! An abstract for my course is now available on the website, and registration is open.

Selected Publications

ACM
Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma

Chelsea Edmonds and Lawrence C. Paulson

In Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, London, UK, 2024

Distinguished Paper Award Abs DOI Bib HTML

Top 10% of accepted papers

Formalised libraries of combinatorial mathematics have rapidly expanded over the last five years, but few use one of the most important tools: probability. How can often intuitive probabilistic arguments on the existence of combinatorial structures, such as hypergraphs, be translated into a formal text? We present a modular framework using locales in Isabelle/HOL to formalise such probabilistic proofs, including the basic existence method and first formalisation of the Lovász local lemma, a fundamental result in probability. The formalisation focuses on general, reusable formal probabilistic lemmas for combinatorial structures, and highlights several notable gaps in typical intuitive probabilistic reasoning on paper. The applicability of the techniques is demonstrated through the formalisation of several classic lemmas on the existence of hypergraphs with certain colourings.
@inproceedings{10.1145/3636501.3636946, author = {Edmonds, Chelsea and Paulson, Lawrence C.}, title = {Formal Probabilistic Methods for Combinatorial Structures using the Lov\'{a}sz Local Lemma}, year = {2024}, isbn = {9798400704888}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, doi = {10.1145/3636501.3636946}, booktitle = {Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs}, pages = {132–146}, numpages = {15}, keywords = {probability, hypergraph colourings, formalisation of mathematics, combinatorics, Lov\'{a}sz local lemma, Isabelle/HOL, Interactive theorem proving}, location = {London, UK}, series = {CPP 2024}, }