I am a Distinguished Postdoctoral Fellow at Northeastern working with Amal Ahmed. Before this I completed a PhD with Nate Foster, and before that I was an undergrad with Zach Tatlock.
My last name sounds like “DEN-jis” when I say it out loud. My full name anagrams to “try heron agendas”.
You can contact me in these places:
Research
I study the theory of programming languages with resources (memory, time, randomness). I am particularly interested in the design and semantics of higher-order languages with substructural (linear, affine, or bunched) type systems. Current projects include
- Type-preserving compilation of a Rust-like "borrow calculus."
- A logical relation for concurrent termination.
- A program logic for higher-order probabilistic programs.
My thesis was a study of the P4 network programming language. We gave it formal semantics, proved that all well-typed programs terminate, and developed both automated and manual verification frameworks grounded in mechanized (Rocq fka Coq) models of the semantics.
Papers
- Qinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer and Andrew W. Appel. Foundational Verification of Stateful P4 Packet Processing. In ITP 2023. [ doi ]
- Rudy Peterson, Eric Hayden Campbell, John Chen, Natalie Isak, Calvin Shyu, Ryan Doenges, Parisa Ataei, and Nate Foster. P4Cub: A Little Language for Big Routers. In CPP 2023. [ doi ]
- Ryan Doenges, Tobias Kappé, John Sarracino, Nate Foster, and Greg Morrisett. Leapfrog: Certified Equivalence for Protocol Parsers. In PLDI 2022. [ doi | arxiv (+proofs) ]
- Ryan Doenges, Mina Tahmasbi Arashloo, Santiago Bautista, Alexander Chang, Newton Ni, Samwise Parkinson, Rudy Peterson, Alaia Solko-Breslin, Amanda Xu, and Nate Foster. Petr4: Formal Foundations for P4 Data Planes. In POPL 2021. [ doi | arxiv (+proofs) ]
- Hardik Soni, Myriana Rifai, Praveen Kumar, Ryan Doenges, and Nate Foster. Composing Dataplane Programs with μP4. In SIGCOMM 2020. [ doi ]
- Ryan Doenges, James R. Wilcox, Doug Woos, Zachary Tatlock, and Karl Palmskog. Verification of Implementations of Distributed Systems Under Churn. In CoqPL Workshop 2017. [ sigplan copy ]
Reviewing
- Artifact evaluation committee, ESOP/FASE/FoSSaCS 2024
- External reviewer, CSL 2024
- External reviewer, CPP 2024
Teaching
- Fall 2022: TA-Instructor (coteaching with Michael Clarkson) for CS 3110.
- Spring 2018: TA for CS 4120.
- Fall 2017: TA for CS 3410.
- Winter 2017: TA for CSE 341.
Service
- 2021–2023: Co-organizer for LGBTea with Andy Ricci and Griffin Berlstein
- 2018–2019: Co-organizer for Grad Seminar with Oli Richardson
- 2021–2022: CS PhD Admissions Committee for Fall 2022