- PhD Student
I am a PhD Student (passed viva, awaiting approval of minor corrections) 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 was a member of the ALEXANDRIA project group team investigating large scale formal proof for the working mathematician. My PhD research work focused on the formalisation of combinatorial structures and proof techniques. I am grateful to have been fully funded for my PhD studies by a Cambridge Australia Scholarship, under the Cambridge Trust, and a studentship from the Department of Computer Science.
Post my PhD submission, I am now a Research Associate in Formal Modelling and Verification in the Department of Computer Science at the University of Sheffield. I'm looking forward to applying my Isabelle and mathematical background to explore a slightly more applied avenue of research, including concepts across software engineering formal methods and security. My new profile and contact details will be available here.
Beyond my research, I greatly enjoy roles in the service, education and outreach aspects of Higher Education. While at Cambridge, I supervised several courses in the Computer Science Tripos at multiple colleges, and was the Mentoring and Outreach Officer for Women@CL for two years. In the 22/23 academic year I was also the President of the Darwin College Student's Association (DCSA) - the Darwin equivalent of an "MCR" in Cambridge terms! Additionally, I was 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 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.
Research
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: https://talks.cam.ac.uk/show/index/164015
- [upcoming]. Oxbridge Women in Computer Science 2023: An introduction to formal verification in Isabelle/HOL. Leading 30 minute workshop.
Themes
Teaching
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
Awards/Memberships
- Academic Awardee from the British Federation of Women Graduates in 2022
- Associate Fellow of Advance HE, following participation in the Cambridge Teaching Associates' Programme 2021/22
- Cambridge Australia Scholar (Full international PhD scholarship for 3 years, jointly funded with the department of computer science).
Positions
- 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.
Conferences/Journals
- POPL 2023 Conference Volunteer
- Session Chair Isabelle Workshop 2022
- Reviewer for the Journal of Automated Reasoning 2022.
Publications
Isabelle Archive of Formal Proofs:
- Hypergraph Colouring Bounds, September 2023
- Probabilistic Method for Combinatorics and the Lovasz Local Lemma, September 2023
- Hypergraphs, September 2023
- The Balog Szemerédi Gowers Theorem (with Angeliki Koutsoukou-Argyraki & Mantas Bakšys), November 2022
- Undirected Graph Theory, September 2022
- Fisher's Inequality: Linear Algebraic Proof Techniques for Combinatorics, April 2022
- Roth's Theorem (with Angeliki Koutsoukou-Argyraki & Lawrence Paulson), December 2021.
- Szemerédi's Regularity Lemma (with Angeliki Koutsoukou-Argyraki & Lawrence Paulson), November 2021.
- Combinatorial Design Theory, August 2021.
- Lucas' Theorem, April 2020.
Conference Presentations (No Proceedings)
- Isabelle Workshop 2020: Lucas's Theorem: Formalising Generating Function Proofs. Paper can be accessed online: https://sketis.net/isabelle/isabelle-workshop-2020
Paper preprints:
- Formal Probabilistic Methods for Combinatorial Structures in Isabelle/HOL (with Lawrence Paulson), available on arxiv from September 2023
