Publications

Conference and journal papers

• Canonicity for Indexed Inductive-Recursive Types, POPL 2026.
• Closure-Free Functional Programming in a Two-Level Type Theory, ICFP 2024. Code supplement.
• 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, LMCS, 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.

PhD thesis

Type-Theoretic Signatures for Algebraic Theories and Inductive Types.

MSc thesis

A Machine-Checked Correctness Proof Of Normalization by Evaluation for Simply Typed Lambda Calculus, 2017, formalization.