Paul He

Photo Email:
Office: Levine 514
Office hours: see calendar

Links: Github | Google Scholar | dblp

I’m a third year PhD student at the University of Pennsylvania in the department of computer and information science, advised by Steve Zdancewic, and a part of PL Club. I do research in the field of programming languages.

I did my undergrad in computer science at the University of Waterloo, where I was in the co-op program. I did software engineering internships at Kongsberg Geospatial, The Coalition, Improbable, and Microsoft. I also did research with Ondřej Lhoták and Vijay Ganesh.




Automata, Computability, and Complexity - CIS 262 (Instructor): Summer 2020
C++ Programming - CIS 190 (Instructor): Fall 2019, Spring 2020
Compilers - CIS 341 (TA): Spring 2020


Algebra for Honours Mathematics - MATH 135 (Undergraduate Marker): Fall 2014

I wasn’t able to TA much during my undergrad. I did do some one on one tutoring for a variety of computer science and math courses during the last few years of undergrad. My favourite to tutor (and most often tutored) was Algorithms (CS 341).


“with …” means the authors are ordered alphabetically.

An Equational Theory for Weak Bisimulation via Generalized Parameterized Coinduction
Yannick Zakowski, Paul He, Chung-Kil Hur, Steve Zdancewic
CPP 2020, New Orleans, USA
paper | 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
paper | 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.
paper | 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
paper | doi | proof | talk