I am a PhD candidate in the Languages, Systems, and Data Lab at the University of California Santa Cruz advised by Lindsey Kuper.
My research explores the design, implementation, and verification of distributed systems and pure functional runtimes. I want to bring software verification to industry.
I have several years of industry experience conceptualizing, developing, and deploying high-availability distributed-systems and machine prediction at scale for Twitch (Amazon), Prismatic (defunct), and Vlingo (Nuance).
Here are some highlights from my CV:
Core
ECS (OOPSLA25; doi; artifact; with
appendices)
Formalization of the ECS pattern and precise characterization of
concurrency that ECS frameworks tend to leave on the table.
Chimeric Consensus (LSD Seminar, 9 May 2025; talk) An accessible intro to consensus, and a brief explanation of SCP’s quorum protocol. The audience was super interactive!
Exceptional
Actors (Haskell23; doi; artifact)
I demonstrate that the GHC Haskell RTS has an actor programming model
hidden in its asychronous exception system. The talk generated
some feedback:
Verifying
CBCAST (IFL22; doi; code)
I expressed a causal message-delivery property as a refinement
type and verified that an implementation of a causal delivery
algorithm delivers messages in causal order, with collaborators at
UCSC and IMDEA.
Tracking
Larva (Science Signalling 10, no. 477; doi; code)
I wrote a deterministic point tracker for a larval-crawling autism
therapy drug assay for work with researchers at UCSF.
Edge Allocator — At Twitch I replaced the system which allocates video edge servers to content streams. The new system required less hardware and fixed overcommitting of edge servers.
Service Authorizer — I created a system to
provide AWS credentials to all bare-metal servers at Twitch. Folks
called it magic
because it integrated seamlessly with the AWS
SDK.
I couldn’t do any of this alone. I collaborate with many people and they have cool websites. Here they are in reverse-chronological order:
| Affiliation | Name | Website |
|---|---|---|
| SDF | Giuliano Losa | https://losa.fr/ |
| UMD | José Manuel Calderón Trilla | http://jmct.cc/ |
| UCSC | Jonathan Castello | https://www.jonathan.com/ |
| UCSC | Gan Shen | https://gshen42.github.io/ |
| UCSC | Lindsey Kuper | https://decomposition.al/ |
| IMDEA | Niki Vazou | https://nikivazou.github.io/ |
| UMD | Michael Hicks | https://www.cs.umd.edu/~mwh/ |
| UMD | Yiyun Liu | https://electriclam.com/ |
| UMD | James Parker | https://jamesparker.me/ |
| UCSF | Akiko Hata | https://profiles.ucsf.edu/akiko.hata |
| UCSF | Risa Kashima | https://orcid.org/0000-0002-9944-0481 |
