Hello!

I am a Ph.D. student in Computer Science Department at Carnegie Mellon, currently working on logic and programming language theory under the supervision of Robert Harper. I enjoy demonstrating correctness of whatever since it can be intellectually challenging, and some of my work happens to have research value. I was previously advised by Jeannette Wing and Avrim Blum for research in privacy.


Research Projects

  1. Homotopy Type Theory

This new foundation seeks new connections between category theory, homotopy theory and type theory.

  • Covering Spaces in Homotopy Type Theory with Robert Harper at TYPES 2014.

The SVG slides and their PDF export. The PDF abstract draft.

  • Covering Spaces in Homotopy Type Theory with Robert Harper at CHomotopy 2013.

The SVG slides and their PDF export. The PDF abstract draft.

  1. Logic Programming for Social Networking Sites with Jeannette Wing

Understanding epistemic consequences in social networking sites through focused linear logic.

  • Logic Programming with Global Information, Names and List Comprehension with Robert Harper and Jeannette Wing. The PDF draft. (This is an INCOMPLETE manuscript in progress.)
  1. Type Refinements with Robert Harper

We show how refinements, introduced by Freeman and Pfenning, elegantly capture invariants required in correctness proofs. We also give the first correctness proof of compiling System F polymorphism to dynamic typing as a concrete example.


Other Talks


Teaching