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!
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 nerd stuff in Lean, here are other things I have been:
- Baking - I'm not very good but at least I haven't made anything truly inedible (yet).
- Poll Worker - I've been a Majority Inspector of Elections (that means I check for people in the books, hand out ballots, help with scanning, etc.) in Allegheny County since the 2024 general primary election.
Random Links (in no particular order):
- Ginkgo Collective
- 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).
