Currently, I'm extending a program logic for reasoning about concurrent, randomized programs. These programs are common in distributed systems (e.g., leader election), yet remain highly error-prone. In the past, I have worked on several different projects. Below is a summary of select past projects; a full list of publications is available here.

wNetKAT

A domain-specific language for verifying quantitative network behavior (e.g., latency, bandwidth, reliability). We compile programs to automata and develop decision procedures for automatically establishing upper and lower bounds across network topologies. Our paper is currently under submission at PLDI 2026; we are also developing a correct-by-construction compiler and implementing our decision procedures in Lean.

(Co)Effects in CBPV

A type system that bounds the effects (e.g., printing) a program may have at runtime, as well as the demands (e.g., resource usage) it may place on its environment. We use our type system to justify the correctness of certain compiler optimizations; everything is fully mechanized in Rocq. Our paper appeared at OOPSLA 2024 and it is available here.

> See code

Logical Relations in Agda

A tutorial paper on the proof technique of logical relations—common in compiler correctness arguments—featuring mechanized proofs by logical relations written in Agda.

Our paper grew out of a mechanized tutorial I wrote showing the correctness of normalization-by-evaluation (an algorithm used for typechecking dependently-typed programming languages).

... and more

As a senior software engineer at Strava, I led both the design and development of several projects: an overhaul of a core data model (using Apache Thrift, MySQL, and Ruby on Rails), a data-export tool for city planners (using Apache Spark and Apache Kafka), and a Scala microservice for all of Strava's static map capabilities.