Hi! I'm Thea (she/her). I use computers sometimes and particularly I am interested in formal verification. If you've been outside and don't know what that means: basically computers go "beep boop" sometimes; what if we knew exactly, with 100% mathematical certainty, when computers go "beep boop". That's what formal verification is trying to solve. Hope that helps!
Currently I am employed as a Research Engineer at rabbit doing work on formal methods and programming languages.
In my freetime I have been using Lean to reason about programming languages and compilers. To this end, I am currently working on C0deine: a work-in-progress, verified compiler from C0 to WebAssembly as well as a bunch of adjacent Lean packages. For more info on what I am working/have worked on see my projects page.
Highlighted Posts:
Provable Standard ML Programs in Lean - A subset of Standard ML, including dynamic semantics, is implemented in Lean 4. Using a variety of newly implemented tactics, this allows for writing machine checkable proofs about SML code similarly to how one would on paper.
Personal Stuff:
Beyond doing computer science nerd stuff in Lean, here are other things I have been doing:
- Baking - I'm not very good but I have a sourdough starter that I use and mediocre fresh bread is still fresh bread :)
- Poll Worker - I was a majority inspector of elections for the 2024 Allegheny County general primary and intend to continue being a poll worker in future elections :3
- History - Recently I've been trying to learn more about trans/queer history and theory, kinda sad sometimes but also important in my opinion.
Random Links (in no particular order):
- Erin in the Morning - Independent journalist that focuses mostly on trans related things.
- QZAP - The Queer Zine Archive Project preserves and distributes queer zines (categorised by year and city).
- Toilet Training (Law and Order in the Bathroom) - A 2003 documentary about "the persistent discrimination, harassment, and violence that people who transgress gender norms face in gender segregated bathrooms" (Sylvia Rivera Law Project).
