Publications

“with …” means the authors are ordered alphabetically.

Semantics for Noninterference with Interaction Trees
Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, Steve Zdancewic
ECOOP 2023, Seattle, USA
:star: Distinguished Paper Award
pdf | doi | code | artifact

Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq
with Nicolas Chappe, Ludovic Henrio, Yannick Zakowski, and Steve Zdancewic
POPL 2023, Boston, USA
pdf | doi | code | talk

A Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs
Paul He, Eddy Westbrook, Brent Carmer, Chris Phifer, Valentin Robert, Karl Smeltzer, Andrei Ştefănescu, Aaron Tomb, Adam Wick, Matthew Yacavone, Steve Zdancewic
OOPSLA 2021, Chicago, USA
pdf | doi | proofs | verification tool | talk

An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction
Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic
CPP 2020, New Orleans, USA
pdf | doi | gpaco code | euttG code | talk

Interaction Trees: Representing Recursive and Impure Programs in Coq
Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, Steve Zdancewic
POPL 2020, New Orleans, USA
:star: Distinguished Paper Award
pdf | doi | code | talk

The Satisfiability of Word Equations: Decidable and Undecidable Theories
with Joel Day, Vijay Ganesh, Florin Manea, and Dirk Nowotka
RP 2018, Marseille, France
pdf | doi

A Simple Soundness Proof for Dependent Object Types
Marianna Rapoport, Ifaz Kabir, Paul He, Ondřej Lhoták
OOPSLA 2017, Vancouver, Canada
:star: Distinguished Artifact Award
pdf | doi | proof | talk

Thesis

Rely-Guarantee Semantics for Separation-Logic-Based Specification Extraction
PhD Thesis, 2024, University of Pennsylvania
pdf | Penn-hosted version | proof