About
I am a final-year undergraduate studying Computer Science and Mathematics at the University of Edinburgh hoping to get into research. My research interests include (dependent) type theory, interactive theorem proving, automated reasoning, formal logic, program verification, denotational semantics, domain theory, universal algebra, and applied category theory.
Experience
Summer Research Fellow
July 2026 – August 2026
Programming Language Foundations Lab, ETH Zürich
Supervisors: Prof. Ralf Jung, Max Vistrup
- Implemented Lean language keywords for defining recursive and inductive predicates within the Iris separation logic using fixpoints, making definitions within the logic as simple as in the meta-logic.
- Built fully automated proof procedures for fixpoint conditions using typeclasses and heuristics.
- Studied category-theoretic generalisations of domain theory used for the Iris model.
- Highly competitive fellowship with an acceptance rate under 1%.
Scientific Intern
June 2025 – August 2025
Programming Languages and Verification Group, IST Austria
Supervisor: Prof. Michael Sammler
- Contributed to porting the Iris project for program verification from Rocq to Lean, making use of its metaprogramming and automation capabilities.
- Implemented the crucial
iapply and irevert tactics for interactive proofs in separation logic, since used over 1000 times across the project.
- Studied the foundations of programming language theory and read contemporary papers in the field.
Education
University of Edinburgh
September 2023 – May 2027
Computer Science and Mathematics (BSc Hons)
- Topics studied include programming language theory, theoretical computer science, and abstract algebra.
- Dissertation will be supervised by Dr Paul Jackson and be about the application of the Lean theorem prover to programming languages.
- Attending talks, workshops, and seminars on current programming language research.
- Consistent top marks, on track for a first-class degree.
Teaching
Teaching Support Provider
September 2024 – Current
School of Informatics, University of Edinburgh
- Introduction to Computation (INF1A): Teaching Assistant, Tutor, and Marker
- Object Oriented Programming (INF1B): Tutor, Marker, and Lab Demonstrator
- Introduction to Algorithms and Data Structures (INF2-IADS): Tutor and Lab Demonstrator
