I am a security and infrastructure researcher at Bloomberg primarily working in software verification. My more general research interests include the fields of categorical logic and programming language theory with a particular focus on type theory.

Research

Papers and Preprints

• Bicubical Directed Type Theory. Ph.D. Thesis, 2024. [pdf]
• A Constructive Model of Directed Univalence in Bicubical Sets. LICS, 2020. (with D. Licata). [pdf]
• Certified code generation from CPS to C (with O. Savary Bélanger and A. Appel). preprint, 2019. [pdf]
• Finite Inverse Categories as Signatures (with D. Tsementzis). arXiv preprint arXiv:1707.07339, 2018. [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]

Talks and Workshops

• Crane Lowers Rocq Safely into C++ (With J. Korkut). RocqPL, 2026.[pdf] [slides] [video]
• Theory and Implementation of Bicubical Directed Type Theory. HoTT, 2023.
• Deciding the Cofibration Logic of Cartesian Cubical Type Theories (With D. Licata and R. Rose). TYPES, 2022. [pdf]
• Directed Higher Inductive Types in Bicubical Directed Type Theory. HoTT/UF (invited keynote), 2021.
• A Constructive Model of Directed Univalence in Bicubical Sets. International Congress on Mathematical Software, 2020.
• A Constructive Model of Directed Univalence in Bicubical Sets. HoTTEST (invited lecture), 2020. [slides][video]
• A Model of Type Theory with Directed Univalence in Bicubical Sets. HoTT, 2019. [slides]
• Bicubical Directed Type Theory. General Examination, 2018. [pdf] [slides]
• Bicubical Directed Type Theory. MURI Meeting, 2018. [slides] [video]
• Unfolding FOLDS (with D. Tsementzis). HoTT/UF, 2017. [pdf] [slides]
• 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 I learned from building an online teaching tool (with L. D'Antoni, R. Alur, D. Kini, M. Viswanathan, S. Gulwani, B. Hartmann). PLOOC, 2015.

Check out some of my contributions to the UniMath Library: here, here, and here.

Teaching

I was an instrutor for the following course:

• Independent Study: Category Theory (Princeton University. Fall 2018, Fall 2021)

I was a teaching assistant for the following courses:

• COS 226: Data Structures and Algorithms (Princeton University. Spring 2019)
• COS 326: Functional Programming (Princeton University. Fall 2018)
• CIS 500: Software Foundations (University of Pennsylvania. Spring 2016)
• CIS 261: Discrete Probability, Stochastic Processes, and Statistical Inference (University of Pennsylvania. Fall 2014, Fall 2015)
• CIS 160: Mathematical Foundation of Computer Science (University of Pennsylvania. Summer 2014, Summer 2015)

Education

• Ph.D. in Computer Science. Princeton University, 2024.
• M.A. in Computer Science. Princeton University, 2018.
• B.A. in Mathematics. University of Pennsylvania, 2015.