Chelsea L. Edmonds

Department of Computer Science

Regent Court

University of Sheffield

Sheffield, UK

Welcome! I’m Chelsea, a postdoctoral Research Associate in Verification at the University of Sheffield. My primary research interests are formalised mathematics, proof assistants (particularly Isabelle/HOL), and formal methods for security and concurrency. In my current position, I’m working on the COVERT project to develop verification tools and models for reasoning on the security of programs running on advanced architectures.

Previously, I completed my PhD at the University of Cambridge under the supervision of Prof. Lawrence C. Paulson. My PhD explored how we can develop modular, flexible and extensible libraries for formalised mathematics (particularly combinatorics) in Isabelle/HOL, and the process for mirroring human intuitive proof techniques in a formal environment. 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.

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

Jun 14, 2024	I was invited to give a talk on my PhD work at a EuroProofNet workshop on Proof Systems for Mathematics and Verification at EPFL. Great event, thank you very much to the organisers for hosting and the invitation!
Jun 05, 2024	I’ve been officially approved for my PhD degree, following approval of minor corrections and final submission.
Apr 18, 2024	I’ve been selected as a participant for the 11th Heidelberg Laureate Forum in September this year. Looking forward to sharing more about the event later in the year.
Apr 14, 2024	This website is finally up and running!

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 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}, }