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 | 90 | 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 | 65 | 2019 |

Normalization for multimodal type theory D Gratzer Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer …, 2022 | 42 | 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 | 38 | 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 | 31 | 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 | 17 | 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 | 8 | 2023 |

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 |

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 |

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 |

Under Lock and Key: A Proof System for a Multimodal Logic GA Kavvos, D Gratzer Bulletin of Symbolic Logic 29 (2), 264-293, 2023 | 2 | 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 | 2 | 2023 |