CV

Education

ETH Zurich, Zurich Switzerland
Sep 2023 - Present
M.Sc. in Computer Science
Direct Doctorate Scholarship

Cornell University, Ithaca NY
Aug. 2016 – May 2020
B.A. in Computer Science & Physics
Advised by Adrian Sampson
Magna Cum Laude Computer Science
Dean’s List Fall 2016, Spring 2017, Fall 2017, Spring 2019
Arts & Sciences Tanner Dean’s Scholar

Selected coursework
Formal Verification, Compilers, Programming Languages, Big Data,
Distributed Computing, Functional Programming, Algorithms,
Cryptography, Security, Formal Language Theory, Operating Systems

Publications

P4Cub: A Little Language for Big Routers
Rudy Peterson, Eric Hayden Campbell, John Chen, Natalie Isak, Calvin Shyu, Ryan Doenges, Parisa Ataei, and Nate Foster.
CPP 2023

Petr4: Formal Foundations for P4 Data Planes
Ryan Doenges, Mina Tahmasbi Arashloo, Santiago Bautista, Alexander Chang, Newton Ni, Samwise Parkinson, Rudy Peterson, Alaia Solko-Breslin, Amanda Xu, Nate Foster.
POPL 2020

Research Experience

Logical Atomicity in Iris
Aug 2024 - Present: Student Researcher
Mentor: Ralf Jung
Working on replacing the coinductive definition of logically-atomic hoare triples in Iris to relieve clients’ proof burden to show that atomic updates are preserved in abort cases.

Poulet4 Project
Jan 2021 - Aug 2023: Research Programmer
Mentors: Nate Foster, Andrew Appel
Implemented in Coq the p4cub IR for a verified p4 compiler, including type soundness & semantics-preserving transformations on the IR.
Wrote the type system in Coq for the p4light IR, including type soundness proofs.

Petr4 Project
Jan 2019 - Aug 2020 : Undergrad Research Assistant
Mentors: Nate Foster
Rigorously defined the static semantics of the network programming language p4 in terms of an operational semantics.
Contributed to OCaml-written type-checker.

Teaching

Teaching Assistant
Cornell CIS Spring 2020
CS 4410: Operating Systems

Teaching Assistant
Cornell CIS Spring 2019 – Fall 2019
CS 3110: Functional Programming

Course Consultant
Cornell CIS Fall 2017 – Fall 2018
CS 1110: Introduction to Computing

Projects

Fast Ternary Convolution
Spring 2024

Lambda Cube
May 2021 – June 2022

Verified Type Reconstruction
July – Oct 2021

Tapl Implementations
June – Oct 2020

Xi Compiler
Spring 2020
Built the intermediate code translation.
Composed a dynamic programming tiling algorithm to select x86 instructions. Contributed to dead code elimination, copy propagation, & the live variable analysis.
Built graph coloring for register allocation.
Written in OCaml in a group for 4 for CS 4120 Compilers at Cornell.

CS 5414 Projects
Fall 2019
Built fault-tolerant 3-phase Commit, Paxos, & Clusters of Order-Preserving Servers (COPS) in Golang in a team of 2.
In a team of 2 for CS 5414 Distributed Computing at Cornell.

Critter World
Fall 2017
Java written DSL for a “critter” program, including parsing and interpretation.
``Critters” interact as clients to a game server with a GUI.
In a team of 2 for CS 2112 Honors Object-Oriented Design and Data Structures at Cornell.

Industry Experience

Amazon, Fintech Seattle, WA
SDE Internship
Summer 2019

Skills

Programming Languages
Favorites: Coq, OCaml, Haskell, Agda, Rust
Other: Python, C, Go, Java

Verification Frameworks
Iris, Coq Equations, Viper, Z3

Languages
English (fluent), German (learning)