I am a PhD student 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 runtimes for pure functional languages. I want to bring software verification to industry, where rapidly changing production systems are difficult to verify with traditional manual proof-writing techniques.
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:
Verifying CBCAST (IFL22; doi; code) – I expressed Lamport’s causal 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.
Verifying CRDTs (OOPSLA20; doi; code) – I wrote a server and model-applications to demonstrate verified CRDTs for work with collaborators at UCSC, UMD, 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.
