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. You can read about it in our ASPLOS'23 paper, and we have working demo systems including a Raft-based key-value store.

I am working on a follow-up project, DCal (note: very much pre-alpha), which introduces guided term rewriting into distributed system model compilation. The goal is to allow a developer to explain mismatches between their model and intended working system, such that the compiler can reliably generate that intended system.

Here are also some recent internships:

• 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.

Regardless of how up to date the above ideas are, this website is a catalog of things I've built or thought about. This includes my research projects, talks (including video links when possible), peer-reviewed publications, and over 10 years' worth of electronic music production.

If you're an undergraduate student reading this who wants to get involved in research, feel free to get in touch. We could work out some sort of collaboration, or, failing that, I could at least point you toward someone whose work might be a better fit for your interests.

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