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/security 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.

Beyond my PhD, I am interested in further exploring verification tools in the more applied context of security (including, but not limited to, the use of proof assistants in this domain). I am also broadly interested in the potential for collaborative research opportunities exploring ideas around the HCI elements of formal verification tools, and computer science education.

Talks (no linked publication)

  • 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.
  • Formalisation of Mathematics Seminar Series 2023. The Locale-centric approach for Formalising Mathematical Hierarchies. A new joint seminar series between the Department of Computer Science and Department of Mathematics at Cambridge:
  • [upcoming]. Oxbridge Women in Computer Science 2023: An introduction to formal verification in Isabelle/HOL. Leading 30 minute workshop. 


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 (2014 - 2016)

Professional Activities



  • Darwin College Students Association (DSCA) President 2022/23
  • Student Representative on the University Postgraduate Mental Health Task Force 2023.
  • Women@CL Mentoring & Outreach Co-Chair 2020/21 & 2021/22
  • University of Cambridge Session Leader
  • Computer Science Department Outreach Activity Volunteer.
  • DCSA Sports & Societies Officer 2021/22.
  • Boeing STEM Ambassador 2018 - 2019.
  • Robogals Regional Executive Officer Asia Pacific 2015 - 2018. 
  • UQ Women in Engineering Student Leader 2014 - 2015.


  • POPL 2023 Conference Volunteer
  • Session Chair Isabelle Workshop 2022
  • Reviewer for the Journal of Automated Reasoning 2022.


Isabelle Archive of Formal Proofs: 

Conference Presentations (No Proceedings)

Upcoming Papers:

  • Angeliki Koutsoukou-Argyraki, Mantas Bakšys, and Chelsea Edmonds. 2023. A Formalisation of the Balog–Szemerédi–Gowers Theorem in Isabelle/HOL. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2023). 

Conference proceedings

  • Koutsoukou-Argyraki, A., Bakšys, M. and Edmonds, C., 2023. A Formalisation of the Balog-Szemerédi-Gowers Theorem in Isabelle/HOL CPP 2023 - Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, co-located with POPL 2023,
  • 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