Hi! You are on my home page. You can reach me at me@ryandoeng.es and doengesr@bc.edu, or drop by room 428-I in 245 Beacon Street.
I am a postdoc at Boston College working with Aaron Stump. I am broadly interested in ascribing precise, compositional specifications to programs with side effects. (After all, if they can't do anything, what is there to worry about?) This includes:
- program logics and type systems for low-level and domain-specific languages
- subtyping and type inference for making these systems usable
- models for type systems and program logics
- compiler verification, especially w.r.t. separate compilation
- categorical logic, insofar as it can systematize the foundations of these topics
Background
Previously I have had the pleasure of being a Distinguished Postdoctoral Fellow with Amal Ahmed at the Northeastern PRL and a Ph.D. student with Nate Foster at Cornell. As an undergraduate I worked with Zachary Tatlock at the University of Washington in Seattle.
Doenges is pronounced “DEN-jis.” My full name is an anagram of “try heron agendas.” I am from Olympia.
Papers
-
Foundational Verification of Stateful P4 Packet Processing.
[ doi
]
ITP 2023. Qinshi Wang, Mengying Pan, Shengyi Wang, Ryan Doenges, Lennart Beringer and Andrew W. Appel. -
P4Cub: A Little Language for Big Routers.
[ doi
]
CPP 2023. Rudy Peterson, Eric Hayden Campbell, John Chen, Natalie Isak, Calvin Shyu, Ryan Doenges, Parisa Ataei, and Nate Foster. -
Leapfrog: Certified Equivalence for Protocol Parsers.
[ doi
| arxiv (+proofs)
]
PLDI 2022. Ryan Doenges, Tobias Kappé, John Sarracino, Nate Foster, and Greg Morrisett. -
Petr4: Formal Foundations for P4 Data Planes.
[ doi
| arxiv (+proofs)
]
POPL 2021. Ryan Doenges, Mina Tahmasbi Arashloo, Santiago Bautista, Alexander Chang, Newton Ni, Samwise Parkinson, Rudy Peterson, Alaia Solko-Breslin, Amanda Xu, and Nate Foster. -
Composing Dataplane Programs with μP4.
[ doi
]
SIGCOMM 2020. Hardik Soni, Myriana Rifai, Praveen Kumar, Ryan Doenges, and Nate Foster.
Extended Abstracts
-
Specifying ABIs with Realizability and Type-Preserving
Compilation
[ abstract
]
PriSC 2026. Brianna Marshall, Ryan Doenges, Owen Duckham, Ari Prakash, Maxime Legoupil, Elan Semenova, Lars Birkedal, and Amal Ahmed. -
Substructural Weakest Preconditions in Fibrations.
[ abstract
]
HOPE 2025. John M. Li, Pedro H. Azevedo de Amorim, and Ryan Doenges. -
Verification of Implementations of Distributed Systems Under Churn.
[ abstract ]
CoqPL 2017. Ryan Doenges, James R. Wilcox, Doug Woos, Zachary Tatlock, and Karl Palmskog.
Students
- Tia Vu: Cornell (MS) ⟶ MIT (PhD)
- Rudy Peterson: Cornell (BA) ⟶ ETH Zürich (PhD)
- Amanda Xu: Cornell (BS) ⟶ UW Madison (PhD)
- Samwise Parkinson
- Alex Chang
- Newton Ni
- Alaia Solko-Breslin
- Calvin Shyu