About Me

Hello! I am a third-year Computer Science PhD student at Carnegie Mellon University with a focus on Programming Languages. My current work is on researching interoperability of proof assistants in the theoretical setting. So, less on how to translate Lean into Rocq, and more on how would one build proof assistants from the ground up to be interoperable with each other! As such, I am interested in type theory (including Homotopy Type Theory in particular), computer formalization/proof assistants, and usability and pedagogy.