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:

Random Links (in no particular order):