Conference and journal papers
- Staged Compilation With Two-Level Type Theory, ICFP 2022. Appendix, Implementation.
- Generalized Universe Hierarchies and First-Class Universe Levels, CSL 2022.
- Elaboration With First-Class Implicit Function Types, ICFP 2020.
- Large and Infinitary Quotient Inductive-Inductive Types, LICS 2020, with Ambrus Kaposi.
- For finitary induction-induction, induction is enough, TYPES 2019 post-proceedings, with Ambroise Lafont and Ambrus Kaposi.
- Signatures and Induction Principles for Higher Inductive-Inductive Types, Logical Methods in Computer Science, published February 2020, with Ambrus Kaposi.
- Shallow Embedding of Type Theory is Morally Correct, MPC 2019, with Ambrus Kaposi and Nicolai Kraus.
- Constructing quotient inductive-inductive types, POPL 2019, with Ambrus Kaposi and Thorsten Altenkirch.
- A syntax for higher inductive-inductive types, FSCD 2018, with Ambrus Kaposi. Received award for best paper by junior researchers.
Type-Theoretic Signatures for Algebraic Theories and Inductive Types.
A Machine-Checked Correctness Proof Of Normalization by Evaluation for Simply Typed Lambda Calculus, 2017, formalization.