hi, i'm a professor of cs at cmu working on type theory and programming. most recently i've been working with my students on developing a computational (pl-centric) semantics of higher-dimensional type theory.