Eric Hayden Campbell

Postdoctoral Research Fellow
UToPiA, UTNS @ UT Austin

email: ehc86 [at] cornell [dot] edu

My research focuses on program semantics, verification, and synthesis for open programs. I believe that hands-off formal methods tools can help us precisely reason about dynamically (re)-configurable code.

During my PhD at Cornell University, I focused on a particular kind of open program, networking data plane programs: type checking them, inferring their specs, and generating their configurations. These days, I'm interested in a broader class of open programs, including databases, operating systems, and AI programming systems.

In my free time, I dabble in linguistics, dance, and music.

Publications

Computing Precise Control Interface Specifications
Eric Hayden Campbell, Hossein Hojjat, Nate Foster
OOPSLA. Oct 2024.
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. Jan 2023.
Kleene Algebra Modulo Theories
Distinguished Paper Award!
Michael Greenberg, Ryan Beckett, and Eric Hayden Campbell
PLDI. June 2022.
Dependently-Typed Data Plane Programming
Matthias Eichholz, Eric Hayden Campbell, Matthias Krebs, Nate Foster, Mira Mezini
POPL. January 2022.
Avenir: Managing Data Plane Heterogeneity via Control Plane Synthesis
Eric Hayden Campbell, William T. Hallahan, Priya Srikumar, Carmelo Cascone, Jed Liu, Vignesh Ramamurthy, Hossein Hojjat, Ruzica Piskac, Robert Soulé, J. Nathan Foster
NSDI. April 2021.
Epistemic Semantics in Guarded String Models
Eric Hayden Campbell, Mats Rooth
SCiL. February 2021.
How to Avoid Making a Billion-Dollar Mistake: Type-Safe Data Plane Programming with SafeP4
Matthias Eichholz + Eric Hayden Campbell, Nate Foster, Guido Salvaneschi, Mira Mezini
ECOOP. July 2019.
Injecting Finiteness to Prove Completeness for Finite Linear Temporal Logic
Eric Hayden Campbell, Michael Greenberg
arXiv:2107.06045.
Infiniteness and Linear Temporal Logic
[Undergraduate Thesis]
Eric Hayden Campbell, advised by Michael Greenberg
Pomona College. May 2017.
Constructing Integer Matrices with Integer Eigenvalues
Christopher Towse and Eric Hayden Campbell
The Mathematical Scientist, UK. June 2016.

News

August 23, 2024 The AEC for OOPSLA '24 awarded Capisce Functional, Resusable, and Available!
October 18, 2023 Visited EPFL! Gave a talk about Avenir in Ed's group
January 20, 2023 Co-chairing the new session previews track for POPL. Come see my talk on Relational & Automated Verification on Friday!
March 10, 2022 I gave an invited talk on Avenir at Intel
July 19, 2021 I gave an invited talk on control plane synthesis at CAV's P4 Verification Workshop
May 3, 2021 My invited talk on control plane synthesis at the Simons Institute is live (watch it here)
April 19, 2021 Cornell's CS News interviewed me about Avenir

Blog Posts

May 10, 2023 Symbolic Compilation for GCL:
A Beginner's Guide to GCL and the Weakest Precondition
February 27, 2023 P4 is not going anywhere:
Nick McKeown's Committment to P4
January 26, 2023 Cannibalize your TTL:
A SIGBOVIK paper I didn't write
December 29, 2021 Solving Myst Puzzles with Z3:
How I Got Nerd-Sniped Playing VR Myst over Christmas
July 7, 2019 Teaching Networking Experientally:
How to teach 40 high school students to program networks in 3 days
June 22, 2019 Theoretically Feasible, Practically Exceptional:
Reflections on the NPI Workshop on the Foundations of Routing

Teaching

Summer 2023 Instructor CS 3 at Jane Street AMP
Summer 2022 Instructor CS 3 at Jane Street AMP
Spring 2018 TA OOP and Data Structures at Cornell University
Fall 2017 TA OOP and Data Structures at Cornell University
Spring 2017 TA Database Systems at Pomona College
Fall 2016 TA Programming Languages at Pomona College
Spring 2016 Head TA Intro to CS at Pomona College
Fall 2015 TA Intro to CS at Pomona College