I am a doctoral student of Robert Harper at Carnegie Mellon University studying type theory, programming languages and semantics. Previously I received a B.A. in Linguistics from U.C. Berkeley. My other interests include category theory, topos theory, formalization of mathematics, Assyriology, ancient languages and literature, Marxism-Leninism-Maoism and Mao Zedong Thought.
I study the syntax and semantics of type theory; currently, I am interested in models of higher dimensional type theory as well as guarded dependent type theory. My colleagues and I have developed the RedPRL proof assistant for cartesian cubical type theory. Today, I am studying definitional equivalence, normal forms and type checking for cartesian cubical type theory and guarded dependent type theory.