Self-Introduction 📖

I'm a PhD student in the Systopia and Software Practices labs at the University of British Columbia. My interests relate to programming language design in an applied context, with an ongoing focus on formal modeling languages. I want full-stack verified software development, from modeling the target system to dealing with performance engineering practicalities and maintenance, to be a realistic option for developers. That switch, between modeling concerns and implementation issues, is a particular point of friction that I'm working to alleviate.

My work so far has been as a developer of the PGo project, a compiler for verified distributed system models (see projects page). I am working on a follow-up project, DCal (note: very much pre-alpha), which introduces guided term rewriting into distributed system model compilation.

Here are also some recent internships I took part in:

• I'm currently (September-November'24) visiting Stephan Merz, Horatiu Cirstea, and the rest of the VeriDis team at Inria/Loria in Nancy, France. We're working on extending their work on trace validation, applying it in the context of the PGo compiler and our verified distributed systems.

• In June-August'24, I interned at Microsoft Research Cambridge with the Trieste project group. My mentor was Matthew Johnson, and I also collaborated with Matthew Parkinson, working on improving the technology underlying Trieste (optimizations, bugfixes, demo documentation). The DCal project's architecture is inspired by what I learned here, in terms of building a framework for experimenting with language design.

• In June-August'22, I worked with Markus Alexander Kuppe at Microsoft Research Redmond to produce an interface-level model of Azure Cosmos DB in TLA+. Through this, we explored the use of TLA+ as a documentation tool for the complicated concurrency behavior of cloud services. See our ICSE-SEIP'23 and :login; articles for details.

Have a look around to see various things I've done.

If you're looking to collaborate (perhaps you're an undergrad thinking about research), then feel free to reach out and ask.

Also, check out Martin Hackett, whose paintings I used as part of this website's design.