I am a Ph.D. candidate in computer science at Princeton University.
My research lies within the fields of categorical logic and
programming language theory with a particular focus on type
- Type Theory with Interpretation and the Problem of Infinite Objects (with D. Tsementzis). In
- Finite Inverse Categories as Signatures (with D. Tsementzis). In
- CertiCoq: A verified compiler for Coq (with A. Anand,
A. Appel, G. Morrisett, Z. Paraskevopoulou, R.
Pollack, O. Savary Bélanger, and M.
Sozeau). CoqPL, 2017. [pdf]
- Automata Tutor and what we learned from building an online
teaching tool (with L. D’Antoni, A. Weinert, and R. Alur).
Bulletin of EATCS, 3(117). 2015. [pdf]
Check out some of my contributions to the UniMath Library