Ryan Doenges

Picture of Ryan

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.

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.

Students

These lists are incomplete and under construction right now.

At Cornell

I was an informal mentor to these students, with the exception of Tia Vu, whose masters thesis I supervised.
  • Tia Vu: Cornell (MS) ⟶ MIT PhD
  • Rudy Peterson: Cornell (BA) ⟶ ETH Zürich (PhD)
  • Amanda Xu: Cornell (BS) ⟶ UW Madison (PhD)
  • Alex Chang
  • Newton Ni
  • Alaia Solko-Breslin
  • Calvin Shyu

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

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