skip to content

Department of Computer Science and Technology

  • PhD Student

I am a final year PhD Student in the Programming, Logic, and Semantics group in the Computer Laboratory at the University of Cambridge, and a member of Darwin College. My supervisor is Prof. Larry Paulson, and I'm a member of the ALEXANDRIA project group team investigating large scale formal proof for the working mathematician. My research work is focused on the formalisation of combinatorial structures and proof techniques. I am grateful to be fully funded for my PhD studies by a Cambridge Australia Scholarship, under the Cambridge Trust, and a studentship from the Department of Computer Science. 

Beyond my research, I greatly enjoy roles in the service, education and outreach aspects of Higher Education. I supervise several courses in the Computer Science Tripos at Cambridge at multiple colleges, and was the Mentoring and Outreach Officer for Women@CL for two years. I'm currently the President of the Darwin College Student's Association (DCSA) - the Darwin equivalent of an "MCR" in Cambridge terms! Additionally, I am involved in the University's outreach programs as a Session Leader, where I've helped produce content and given lectures on various topics in mathematics and computer science to senior school students. 


I completed my undergraduate studies from 2012 - 2017 at the University of Queensland, Australia, graduating with First Class Honours and a University Medal from a Bachelor of Engineering (Software) and Bachelor of Science (Mathematics). As part of my degree, I also completed a semester abroad at the University of Edinburgh. Between 2017 - 2019, I was a Software Engineer for Boeing Australia, where I was part of the PhantomWorks International team working on advanced prototyping projects for autonomous systems. While my time at Boeing was an invaluable experience, I found myself missing the opportunities to explore more theoretical concepts as well as my teaching work, which led me to commence my PhD at Cambridge in 2019. 

Beyond my research work, I have been involved in a leadership capacity for many different organisations and initiatives, as evidenced from my current role on the DCSA. One of my most significant roles was as the APAC Regional Executive Officer for Robogals from 2015 - 2018, an international not-for-profit inspiring girls to pursue careers in STEM fields. Outside of work, I enjoy travelling (when possible!), writing, and music. I have a diploma on the violin, and am a member of the Cambridge Ceilidh Band and Cambridge Graduate Orchestra. 


My research interests include interactive proof assistants, the formalisation of mathematics, and software verification. I am currently focusing on the formalisation of new combinatorial structures in Isabelle/HOL, as well as exploring formal techniques we can use to automate and/or simplify the process of formalising common combinatorial proof techniques which rely heavily on human intuition and a broad range of other mathematical topics.

My undergraduate honours project was completed under the supervision of Dr. Larissa Meinicke and Prof. Ian Hayes at the University of Queensland. It investigated the use of Isabelle to verify a concurrency program algebra. I am also broadly interested in research into best practices for computer science education. Although I am not currently active in this field, I would be interested in exploring it more beyond my PhD. 


  • Oxbridge Women in Computer Science 2020: Lucas's Theorem: A Generating Function Proof. Awarded a prize for second best student presentation.
  • University of Queensland "Maths Talks" May 2021:  Maths by Machine: Formal Proof Technology and Combinatorial Challenges. Guest speaker for event jointly hosted by the UQ Maths and UQ Computing societies.


I greatly enjoy teaching, and have supervised several courses since starting my studies at Cambridge:

  • IB Logic & Proof (Lent 2020/2022/2023)
  • IA Discrete Mathematics (Michaelmas 2020/2021, Lent 2020/2021/2022 )
  • IA Algorithms (Lent 2021)
  • IA Software and Security Engineering (Easter 2021/2022)
  • IB Semantics (Michaelmas 2021/2022)

I was honoured to be awarded the Silvia Breu prize for best supervisor in Computer Science at Queens College in the 2021/22 year.

Previously, I was a tutor/demonstrator at the University of Queensland for the following courses:

  • CSSE1001: Introduction to Software Engineering (2015 - 2017)
  • CSSE2002: Software Engineering in the Large (2017)
  • MATH1061: Discrete Mathematics (2015 - 2016)

Professional Activities


Isabelle Archive of Formal Proofs: 

Conference Presentations (No Proceedings)

Conference proceedings

  • Edmonds, C. and Paulson, L., 2022. Formalising Fisher’s Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics LIPIcs : Leibniz International Proceedings in Informatics,
    Doi: 10.4230/LIPIcs.ITP.2022.11
  • Edmonds, C. and Paulson, L., A Modular First Formalisation of Combinatorial Design Theory Intelligent Computer Mathematics 14th International Conference, CICM 2021,
  • Journal articles

  • Edmonds, C., Koutsoukou-Argyraki, A. and Paulson, LC., Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL Journal of Automated Reasoning,
  • Contact Details

    Office phone: 
    (01223) 7-63737