D. Gratzer, M. Møller, L. Birkedal
2024
- Idempotent resources in separation logic: the heart of core in Iris
- 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