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 interests include category theory,
topos theory, formalization of mathematics, Assyriology, ancient
languages and literature, Marxism-Leninism-Maoism and Mao Zedong Thought.
models of guarded dependent type theory.
implementing Computational Higher-Dimensional Type
and practice of proof metalanguages.
Lecture Notes, Tutorials
Together with my co-hosts David Christiansen and Darin Morrison, I helped
create The Type Theory