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.


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

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