My site is pretty minimal so far - mostly a placeholder so the grand linking engines begin to acknowledge me. But here's recent work/research interests:

NilAway (blog announcement, github):

Null dereference freedom in languages can be phrased in terms of very simple constraints. NilAway is a compositional static analysis that incrementally computes and accumulates those constraints, reporting errors to the programmers when contradictions arise. I began work on its design and implementation in 2020 that has since been carried on by an amazing team at Uber. It seems to be very effective so far.

Swift (pitch on evolution forum):

Work on type systems for data race freedom that I undertook with Mae Milano and Andrew Myers has inspired collaboration with the Swift team at Apple. Namely, region-based linear ownership seems to fit naturally onto Swift's actor model, and I have worked to see if this graft can be adopted.

Wisening Assertions (popl src talk, short paper):

Languages can include assertions to give programmers a well-specified way to include correctness reasoning in their code. Unfortunately using these assertions to enforce correctness at runtime is prohibitively expensive because the cost of assertions is paid continuously for the lifetime of the software deployment. I think large code deployments should use their assertions to maintain a live and cheap model of where bugs could live in the running code, and then stop executing assertions that become redundant over time. Doing this in a way that still guarantees arbitrarily high assurance of bug freedom over time, I call "Wisening Assertions".

I've started building out systems for Wisening Assertions, and I like the underlying problem ("hard part") that's arisen as well:

Relate observable probabilistic events about code execution (branch frequency, other runtime monitors) to interesting probabilistic events about code execution (was there information flow? was an unoptimized path hit?)

This problem is in some ways a ripe candidate for ML - "train" a model to predict interesting code events given the observable facts about past executions - but I've been interested in a more basic approach inspired by probabilistic graphical models. It's been illuminating and I also have exciting ideas for applications to speculative compilation.