Paul He

Photo Github

I will be starting my PhD at the University of Pennsylvania in the fall of 2018. I did my undergrad at the University of Waterloo. My research interests lie in programming languages, logic, and the relationship between the two.


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. To appear in RP 2018.

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