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, being one of 20 selected out of over 2500.
- Co-authored "Iris in Lean", currently under review for CPP 2027: arXiv.
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.
