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.
- Homotopy Type Theory
- Social Network Logic with Jeannette Wing
Understanding epistemic consequences in social networking sites through focused linear logic.
- (Random Fun Topics in Programming Language Theory)
- Type Refinements for Compiler Correctness with Robert Harper. The draft (PDF) and full proofs (PDF).
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.
- Teaching Assistant of 15814: Type Systems for Programming Languages, Fall 2012.