D. Gratzer, J. Weinberger, U. Buchholtz
2025
- The Yoneda embedding in simplicial type theory
- Directed univalence in simplicial homotopy type theory
-
D. Gratzer, J. Weinberger, U. Buchholtz
2024 - Weak-head conversion testing for MTT
-
D. Gratzer
2024 - Adjoint modalities in MTT
-
D. Gratzer
2024 - Controlling unfolding in type theory
-
D. Gratzer, J. Sterling, C. Angiuli, T. Coquand, L. Birkedal
2022 - Denotational semantics of general store and polymorphism
- Strict universes for Grothendieck topoi
- The directed plump ordering
- An inductive-recursive universe generic for small families
- Crisp induction for intensional identity types
-
D. Gratzer
2021 - Syntactic categories for dependent type theory: sketching and adequacy
- An Addendum to Section 7 of First Steps in Synthetic Guarded Domain Theory
-
D. Gratzer
2018 - Formalizing Concurrent Stacks With Helping: A Case Study In Iris