I'm currently working as a security researcher at Bloomberg, applying formal methods in industry.

I'm also a PhD candidate in computer science at Princeton University's programming languages group, advised by Andrew W. Appel, working on VeriFFI, a foreign function interface between Coq and C, on the CertiCoq compiler, verified via VST. I plan to graduate in 2024.

I'm interested in compilers, type systems, formal verification, metaprogramming, and symbolic natural language processing.

Before starting a PhD program, I was at Wesleyan University (BA, MA), working with Daniel R. Licata on compiler verification and editor interaction for dependently typed languages.

You can reach me at joomy@type.systems, or look at my CV, or my Twitter and Mastodon posts.