Ryan Doenges

Hi! You are on my home page. You can reach me at me@ryandoeng.es and doengesr@bc.edu. I am a postdoc at Boston College with Aaron Stump.

I design new semantics, logics, and type systems to support high-level reasoning about low-level programs. I am especially interested in application domains that play foundational roles in computing, like networking and language runtimes, and concepts that play foundational roles in verification, like predicate transformers and resource algebras.

News

10/26

I am off to the UK for a research visit to Pedro Amorim at the University of Bath.

9/26

I gave a talk at the MIT FLAME lab on semantics for combinational cycles.

8/26

I'm at ICFP in Indianapolis to present our Haskell Symposium paper.

Papers

• Coercive Subtyping for Implicit Functorial Programming. [ doi ]
  HASKELL 2026. Ryan Doenges, Caden Parajuli, Ayden Lamparski, Ke Wu, and Aaron Stump.
• 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

Reviewing

• 2027: CSL (external)
• 2026: TOPLAS, ESOP (external)
• 2025: LICS (subreviewer)
• 2024: CSL (external), CPP (external), ESOP/FASE/FoSSaCS (AEC)