Hello!

Hi my name is Rudy. I study programming languages and interactive theorem-proving. I’m interested in separation logic, dependent type theory, and proof assistants such as Rocq, Lean, and Agda. I will be starting a PhD at EPFL in February 2026.

I am a Master’s student at ETH Zürich. Currently, I am working on mechanizing weighted formal language theory in Lean, supervised by Franz Nowak and Juan Luis Gastaldi. I completed my Master’s thesis A Program Logic for Tree Borrows, a mechanized program logic in Iris, and experimented with logical atomicity in Iris, both supervised by Ralf Jung.

Previously I completed my Bachelor’s at Cornell University where I was advised by Professor Adrian Sampson. I worked on formalizing P4’s semantics in Rocq for the Petr4 and Poulet4 projects under Professor Nate Foster. Furthermore I collaborated with Professor Andrew Appel on building a type system for P4 in Rocq.

I like travel and cats (see Pico in the photo)!

You can reach me via email at the following:

concat ["rpeterson", "@", "ethz.ch"]