skip to content

Department of Computer Science and Technology

  • PhD Student

I am a third year PhD Student in the Programming, Logic, and Semantics group in the Computer Laboratory at the University of Cambridge. 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 education and outreach. I supervise several courses in the Computer Science Tripos at Cambridge, and am a member of the Women@CL Committee. 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. 

Biography

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 also been involved in many STEM Education and Diversity initiatives. Most significantly, I spent 3 years as the APAC Regional Executive Officer for Robogals, 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. 

Research

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. 

Presentations/Talks

  • 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.

Teaching

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

  • IB Logic & Proof (Lent 2020/2022)
  • 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)

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

Publications

Isabelle Archive of Formal Proofs: 

Conference Presentations (No Proceedings)

Journal articles

  • Edmonds, C., Koutsoukou-Argyraki, A. and Paulson, LC., 2022. Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL
  • Conference proceedings

  • Edmonds, C. and Paulson, L., A Modular First Formalisation of Combinatorial Design Theory Intelligent Computer Mathematics 14th International Conference, CICM 2021,
  • Edmonds, C. and Paulson, L., Formalising Fisher’s Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics
  • Contact Details

    Room: 
    FE07
    Office phone: 
    (01223) 7-63737
    Email: 

    cle47@cam.ac.uk