Publications

“with …” means the authors are ordered alphabetically.

Choice Trees: Representing and Reasoning About Nondeterministic, Recursive, and Impure Programs in Rocq
with Nicolas Chappe, Ludovic Henrio, Eleftherios Ioannidis, Yannick Zakowski, and Steve Zdancewic
Journal of Functional Programming, 2025 (Extended journal version of POPL 2023 paper)
pdf | doi | code

Semantics for Noninterference with Interaction Trees
Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, Steve Zdancewic
ECOOP 2023, Seattle, USA
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
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
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