I am a postdoctoral in Carnegie Mellon University, interested in mechanized reasoning and many topics in programming language theory. Currently I am mainly working on computational higher-dimensional type theory.