Paul He

Photo Github
Google Scholar

I’m a first 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.


Word Equations

I worked with Vijay Ganesh on word equations (aka the theory of concatenation, theory of strings, or equations in free monoids). We investigated decidability questions for various fragments and extensions of word equations. We also worked on the Z3str3 string solver and a tool for generating problem instances for strings.


I worked with Ondřej Lhoták on dependent object types (DOT), a calculus modelling the Scala programming language. We simplified the existing proof to be easier to extend and modify. We also extended a version of DOT with mutation with a new non-null type.


“with …” means the authors are ordered alphabetically.

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
Work In Progress
arxiv | code

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

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
paper | doi | proof