| 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 | 81 | 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 | 60 | 2019 |
| Normalization for multimodal type theory D Gratzer Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer …, 2022 | 36 | 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 | 36 | 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 | 30 | 2019 |
| Cubical Syntax for Reflection-Free Extensional Equality J Sterling, C Angiuli, D Gratzer 4th International Conference on Formal Structures for Computation and …, 2019 | 30 | 2019 |
| 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 | 17 | 2022 |
| A cubical language for Bishop sets J Sterling, C Angiuli, D Gratzer Logical Methods in Computer Science 18, 2022 | 17 | 2022 |
| Strict universes for Grothendieck topoi D Gratzer, M Shulman, J Sterling arXiv preprint arXiv:2202.12012, 2022 | 17 | 2022 |
| Syntactic categories for dependent type theory: sketching and adequacy D Gratzer, J Sterling arXiv preprint arXiv:2012.10783, 2020 | 17 | 2020 |
| A stratified approach to Löb induction D Gratzer, L Birkedal 7th International Conference on Formal Structures for Computation and …, 2022 | 13 | 2022 |
| Type theory à la mode D Gratzer, GA Kavvos, A Nuyts, L Birkedal | 9 | 2020 |
| Denotational semantics of general store and polymorphism J Sterling, D Gratzer, L Birkedal arXiv preprint arXiv:2210.02169, 2022 | 8 | 2022 |
| Controlling unfolding in type theory D Gratzer, J Sterling, C Angiuli, T Coquand, L Birkedal arXiv preprint arXiv:2210.05420, 2022 | 6 | 2022 |
| Syntax and semantics of modal type theory D Gratzer Aarhus University, 2023 | 4 | 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 |
| Iron: Managing obligations in higher-order concurrent separation logic D Gratzer, A Bizjak, R Krebbers, L Birkedal work 29, 15, 2017 | 2 | 2017 |
| Under Lock and Key: A Proof System for a Multimodal Logic GA Kavvos, D Gratzer Bulletin of Symbolic Logic 29 (2), 264-293, 2023 | 1 | 2023 |
| {mitten}: A Flexible Multimodal Proof Assistant P Stassen, D Gratzer, L Birkedal 28th International Conference on Types for Proofs and Programs (TYPES 2022), 2023 | 1 | 2023 |
