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 was previously advised by Jeannette Wing and Avrim Blum.

Research Projects

  1. Social Network Logic with Jeannette Wing

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

  1. Homotopy Type Theory

This new foundation seeks new connections between category theory, homotopy theory and type theory. Check out this blog and my old Agda code and our latest Agda code base.

  1. (Random Fun Topics in Programming Language Theory)

Talks

  1. Logic systems for computer scientists at FLOLAC 2012. The slides (SVG) in Traditional Chinese.

Papers

  1. Correctness of Compiling Polymorphism to Dynamic Typing with Robert Harper (submitted). The draft (PDF) and full proofs (PDF).

We presented the first correctness proof of the usual implementation of polymorphism in dynamic typing.

Teaching

  1. Teaching Assistant of 15814: Type Systems for Programming Languages, Fall 2012.