| Publication | Date of Publication | Type |
|---|
| Set-theoretic and type-theoretic ordinals coincide | 2026-02-27 | Paper |
| A lambda term representation inspired by linear ordered logic | 2025-08-19 | Paper |
| One bit to rule them all -- imperfect randomness harms lattice signatures | 2025-07-29 | Paper |
| On symmetries of spheres in univalent foundations | 2025-06-18 | Paper |
| Path spaces of higher inductive types in homotopy type theory | 2024-12-19 | Paper |
Two-level type theory and applications
Mathematical Structures in Computer Science | 2024-03-05 | Paper |
Two-level type theory and applications - ERRATUM
Mathematical Structures in Computer Science | 2024-03-05 | Paper |
From cubes to twisted cubes via graph morphisms in type theory
(available as arXiv preprint) | 2023-10-27 | Paper |
Connecting constructive notions of ordinals in homotopy type theory
(available as arXiv preprint) | 2023-08-08 | Paper |
Type-theoretic approaches to ordinals
Theoretical Computer Science | 2023-04-27 | Paper |
A rewriting coherence theorem with applications in homotopy type theory
Mathematical Structures in Computer Science | 2023-02-28 | Paper |
| Set-Theoretic and Type-Theoretic Ordinals Coincide | 2023-01-25 | Paper |
Type-Theoretic Approaches to Ordinals
(available as arXiv preprint) | 2022-08-07 | Paper |
A Rewriting Coherence Theorem with Applications in Homotopy Type Theory
(available as arXiv preprint) | 2021-07-04 | Paper |
Coherence via well-foundedness. Taming set-quotients in homotopy type theory
Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science | 2021-01-21 | Paper |
Free higher groups in homotopy type theory
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science | 2021-01-20 | Paper |
Free higher groups in homotopy type theory
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science | 2021-01-20 | Paper |
| Internal $\infty$-Categorical Models of Dependent Type Theory: Towards 2LTT Eating HoTT | 2020-09-03 | Paper |
| Shallow embedding of type theory is morally correct | 2020-05-05 | Paper |
Shallow embedding of type theory is morally correct
(available as arXiv preprint) | 2020-05-05 | Paper |
| Path Spaces of Higher Inductive Types in Homotopy Type Theory | 2019-01-17 | Paper |
Quotient inductive-inductive types
(available as arXiv preprint) | 2018-07-17 | Paper |
Constructions with non-recursive higher inductive types
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science | 2018-04-23 | Paper |
Functions out of higher truncations
(available as arXiv preprint) | 2017-08-31 | Paper |
Extending homotopy type theory with strict equality
(available as arXiv preprint) | 2017-07-19 | Paper |
The general universal property of the propositional truncation
(available as arXiv preprint) | 2017-07-12 | Paper |
| Univalent Higher Categories via Complete Semi-Segal Types | 2017-07-12 | Paper |
Partiality, Revisited
Lecture Notes in Computer Science | 2017-05-19 | Paper |
Notions of anonymous existence in Martin-Löf type theory
(available as arXiv preprint) | 2017-05-08 | Paper |
| Space-Valued Diagrams, Type-Theoretically (Extended Abstract) | 2017-04-14 | Paper |
Higher homotopies in a hierarchy of univalent universes
ACM Transactions on Computational Logic | 2017-01-27 | Paper |
Generalizations of Hedberg's theorem
Lecture Notes in Computer Science | 2013-06-28 | Paper |
