A simple soundness proof for dependent object types. - Marianna Rapoport; Ifaz Kabir; Paul He 002; Ondrej Lhoták (Proc. ACM Program. Lang., 2017)

The Satisfiability of Word Equations: Decidable and Undecidable Theories. - Joel D. Day; Vijay Ganesh 001; Paul He 002; Florin Manea; Dirk Nowotka (RP, 2018)

The Satisfiability of Extended Word Equations: The Boundary Between Decidability and Undecidability. - Joel D. Day; Vijay Ganesh 001; Paul He 002; Florin Manea; Dirk Nowotka (CoRR, 2018)

Interaction Trees: Representing Recursive and Impure Programs in Coq (Work In Progress). - Li-yao Xia; Yannick Zakowski; Paul He 002; Chung-Kil Hur; Gregory Malecha; Benjamin C. Pierce; Steve Zdancewic (CoRR, 2019)

An equational theory for weak bisimulation via generalized parameterized coinduction. - Yannick Zakowski; Paul He 002; Chung-Kil Hur; Steve Zdancewic (CPP, 2020)

Interaction trees: representing recursive and impure programs in Coq. - Li-yao Xia; Yannick Zakowski; Paul He 002; Chung-Kil Hur; Gregory Malecha; Benjamin C. Pierce; Steve Zdancewic (Proc. ACM Program. Lang., 2020)

A type system for extracting functional specifications from memory-safe imperative programs. - Paul He 002; Eddy Westbrook; Brent Carmer; Chris Phifer; Valentin Robert; Karl Smeltzer; Andrei Stefanescu; Aaron Tomb; Adam Wick; Matthew Yacavone; Steve Zdancewic (Proc. ACM Program. Lang., 2021)

Semantics for Noninterference with Interaction Trees. - Lucas Silver; Paul He 002; Ethan Cecchetti; Andrew K. Hirsch; Steve Zdancewic (ECOOP, 2023)

Semantics for Noninterference with Interaction Trees (Artifact). - Lucas Silver; Paul He 002; Ethan Cecchetti; Andrew K. Hirsch; Steve Zdancewic (Dagstuhl Artifacts Ser., 2023)

Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq. - Nicolas Chappe; Paul He 002; Ludovic Henrio; Yannick Zakowski; Steve Zdancewic (Proc. ACM Program. Lang., 2023)

Alternative Grading at Scale: Insights from Implementing Weekly Checkpoint Quizzes in a Large Introductory CS Course. - Sadia Sharmin; Paul He 002 (Koli Calling, 2025)

Choice trees: Representing and reasoning about nondeterministic, recursive, and impure programs in Rocq. - Nicolas Chappe; Paul He 002; Ludovic Henrio; Eleftherios Ioannidis; Yannick Zakowski; Steve Zdancewic (J. Funct. Program., 2025)