Hello!
Hi my name is Rudy. I study programming languages and interactive theorem-proving. I’m interested in compiler verification, formalizing language semantics, dependent type theory, and proof assistants such as Coq and Agda.
I am currently a Direct Doctorate student at ETH Zurich. I am working on logical atomicity in Iris with 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 the Petr4 under Professor Nate Foster. Furthermore I collaborated with Professor Andrew Appel on building a type system for P4.
I like travel, fiction, and cats (see Pico in the photo)!
You can reach me via email at the following: