Paul He
 |
Email: paulhe@cis.upenn.edu Office: Levine 514 Office hours: see calendar Links: Github | Google Scholar | dblp |
I’m a sixth and final 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. In the fall of 2020, I did an internship at Galois working with Eddy Westbrook.
I did my undergrad in computer science at the University of Waterloo, where I was in the co-op program. There, I did research with Ondřej Lhoták and Vijay Ganesh. I also did software engineering internships at Kongsberg Geospatial, The Coalition, Improbable, and Microsoft.
News
- I will be starting as an Assistant Professor, Teaching Stream at the University of Toronto in the fall!
Teaching
Penn
C++ Programming - CIS 1900 (Instructor): Fall 2022, Fall 2021, Spring 2020, Fall 2019
Introduction to Computer Programming - CIS 1100 (Instructor): Summer 2022
Automata, Computability, and Complexity - CIS 262 (Instructor): Summer 2020
Compilers - CIS 341 (TA): Spring 2020
Waterloo
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 my last few years at Waterloo. My favourite to tutor (and most often tutored) was Algorithms (CS 341).
Publications
“with …” means the authors are ordered alphabetically.
Semantics for Noninterference with Interaction Trees
Lucas Silver, Paul He, Ethan Cecchetti, Andrew K. Hirsch, Steve Zdancewic
ECOOP 2023, Seattle, USA
Distinguished Paper Award
paper | doi | code | artifact
Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq
with Nicolas Chappe, Ludovic Henrio, Yannick Zakowski, and Steve Zdancewic
POPL 2023, Boston, USA
paper | doi | code | talk
A Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs
Paul He, Eddy Westbrook, Brent Carmer, Chris Phifer, Valentin Robert, Karl Smeltzer, Andrei Ştefănescu, Aaron Tomb, Adam Wick, Matthew Yacavone, Steve Zdancewic
OOPSLA 2021, Chicago, USA
paper | doi | proofs | verification tool | talk
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
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.
Distinguished Artifact Award
paper | doi | proof | talk