I enjoy making computer science more accessible, whether by writing articles, making fun interactive projects, or just rambling to passers-by. You can check out my blog here.
I have an academic interest in mathematical logic and formal software verification; I'm currently learning the Coq proof assistant.
Imperative mini-language in which programs are axiomatically verified by a Hoare logic-based system that proves validity according to a user-provided program specification. (link)
Delay-Tolerant Link-State Routing
Undergraduate dissertation project for the University of Cambridge. Implementing and evaluating a modified link-state routing protocol in C for real Unix routers that is tolerant to failures of links and nodes in the network. (link)
UK high school-equivalent final-year project for computer science, implementing a triangle mesh renderer in C++ using a spatial-acceleration data structure to reduce the running time from linear to logarithmic in the number of triangles. (link)
- Spring 2023-24 Supervisor for Logic and Proof.
- Autumn 2023-24 Supervisor for Semantics of Programming Languages.
- Summer 2022-23 Supervisor for Hoare Logic and Model Checking.
- Spring 2022-23 Supervisor for Logic and Proof.
- Autumn 2022-23 Supervisor for Introduction to Graphics.
(At Cambridge, supervisions are intensive small-group sessions of 1–3 students where concepts are explored in depth, and form a significant part of the teaching of a course — cam.ac.uk.)