About
I am in my third year at the University of Edinburgh studying Computer Science
and Mathematics. My main interests are in applying rigorous formal methods to programming languages and compilers. In addition, I have a passion for teaching mathematics and computer science!
Iris-Lean
I am a contributor to
Iris-Lean, a port of the Iris higher-order concurrent separation logic framework for the Lean theorem prover. In particular, I am concerned with using metaprogramming to implement the
MoSeL proof interface. As it enables seamless direct modification of the compilation process, Lean metaprogramming is a powerful tool that allows implementing Iris tactics in much the same way common Lean tactics are defined.
Most of the work I did on Iris-Lean was under the invaluable supervision and guidance of Prof. Michael Sammler when I was a Scientific Intern in the
Programming Languages and Verification Group at ISTA.
Teaching Support
◦ Teaching Assistant for Introduction to Computation, administrating automated systems for marking functional programming coursework and maintaining course materials for Haskell and computational logic (Autumn 2025)
◦ Lab Demonstrator for Introduction to Algorithms and Data Structures, instructing students in effective problem solving approaches using algorithms (Autumn 2025, Spring 2026)
◦ Tutor, Marker, and Lab Demonstrator for Object Oriented Programming (Spring 2025)
◦ Tutor and Marker for Introduction to Computation (Autumn 2024)
