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
This new foundation seeks new connections between category theory, homotopy theory and type theory.
- The main website collecting all relevent studies.
- Covering Spaces in Homotopy Type Theory with Robert Harper at TYPES 2014.
- Covering Spaces in Homotopy Type Theory with Robert Harper at CHomotopy 2013.
- 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.)
- 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.
- Logic systems for computer scientists at FLOLAC 2012. The SVG slides and the PDF export in Traditional Chinese.
- Teaching Assistant of 15814: Type Systems for Programming Languages, Fall 2012.