| Multimodal dependent type theory D Gratzer, GA Kavvos, A Nuyts, L Birkedal Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer …, 2020 | 92 | 2020 |
| Implementing a modal dependent type theory D Gratzer, J Sterling, L Birkedal Proceedings of the ACM on Programming Languages 3 (ICFP), 1-29, 2019 | 67 | 2019 |
| Normalization for multimodal type theory D Gratzer Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer …, 2022 | 44 | 2022 |
| Transfinite Iris: Resolving an existential dilemma of step-indexed separation logic S Spies, L Gäher, D Gratzer, J Tassarotti, R Krebbers, D Dreyer, ... Proceedings of the 42nd ACM SIGPLAN International Conference on Programming …, 2021 | 42 | 2021 |
| Iron: Managing obligations in higher-order concurrent separation logic A Bizjak, D Gratzer, R Krebbers, L Birkedal Proceedings of the ACM on Programming Languages 3 (POPL), 1-30, 2019 | 34 | 2019 |
| Cubical Syntax for Reflection-Free Extensional Equality J Sterling, C Angiuli, D Gratzer 4th International Conference on Formal Structures for Computation and …, 2019 | 31 | 2019 |
| A cubical language for Bishop sets J Sterling, C Angiuli, D Gratzer Logical Methods in Computer Science 18, 2022 | 19 | 2022 |
| Strict universes for Grothendieck topoi D Gratzer, M Shulman, J Sterling arXiv preprint arXiv:2202.12012, 2022 | 19 | 2022 |
| Modalities and Parametric Adjoints D Gratzer, E Cavallo, GA Kavvos, A Guatto, L Birkedal ACM Transactions on Computational Logic (TOCL) 23 (3), 1-29, 2022 | 18 | 2022 |
| Syntactic categories for dependent type theory: sketching and adequacy D Gratzer, J Sterling arXiv preprint arXiv:2012.10783, 2020 | 18 | 2020 |
| A stratified approach to Löb induction D Gratzer, L Birkedal 7th International Conference on Formal Structures for Computation and …, 2022 | 14 | 2022 |
| Type theory à la mode D Gratzer, GA Kavvos, A Nuyts, L Birkedal | 10 | 2020 |
| Syntax and semantics of modal type theory D Gratzer Aarhus University, 2023 | 9 | 2023 |
| Denotational semantics of general store and polymorphism J Sterling, D Gratzer, L Birkedal arXiv preprint arXiv:2210.02169, 2022 | 9 | 2022 |
| Controlling unfolding in type theory D Gratzer, J Sterling, C Angiuli, T Coquand, L Birkedal arXiv preprint arXiv:2210.05420, 2022 | 6 | 2022 |
| {mitten}: A Flexible Multimodal Proof Assistant P Stassen, D Gratzer, L Birkedal 28th International Conference on Types for Proofs and Programs (TYPES 2022), 2023 | 3 | 2023 |
| A flexible multimodal proof assistant P Stassen, D Gratzer, L Birkedal Workshop on the Implementation of Type Systems, 2022 | 3 | 2022 |
| An inductive-recursive universe generic for small families D Gratzer https://jozefg.github.io/papers/an-inductive-recursive-universe-generic-for …, 2022 | 3 | 2022 |
| Directed univalence in simplicial homotopy type theory D Gratzer, J Weinberger, U Buchholtz arXiv preprint arXiv:2407.09146, 2024 | 2 | 2024 |
| The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations D Gratzer, H Gylterud, A Mörtberg, E Stenholm arXiv preprint arXiv:2402.04893, 2024 | 2* | 2024 |
