D. Gratzer, J. Weinberger, U. Buchholtz
Logic in Computer Science
2025
- The Yoneda embedding in simplicial type theory
- Idempotent resources in separation logic: the heart of core in Iris
-
D. Gratzer, M. Møller, L. Birkedal
Foundations of Software Science and Computation Structures 2025 - A modal deconstruction of Löb induction
- Unifying cubical and multimodal type theory
- The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations
- Free theorems from univalent reference types
- Syntax and semantics of modal type theory
-
D. Gratzer
PhD Thesis 2023 - Under Lock and Key: A Proof System for a Multimodal Logic
- mitten: flexible multimodal proof assistant
-
P. Stassen, D. Gratzer, L. Birkedal
TYPES 2022 Post-proceedings 2023 - A stratified approach to Löb induction
- Normalization for multimodal type theory
-
D. Gratzer
Logic in Computer Science 2022 - A Cubical Language for Bishop Sets
- Modalities and Parametric Adjoints
- Multimodal Dependent Type Theory
- Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic
- Multimodal Dependent Type Theory
-
D. Gratzer, G. A. Kavvos, A. Nuyts, and L. Birkedal
Logic in Computer Science 2020 - Implementing a Modal Dependent Type Theory
-
D. Gratzer, J. Sterling, and L. Birkedal
International Conference on Functional Programming 2019 - Cubical Syntax for Reflection-Free Extensional Equality
- Iron: Managing Obligations in Higher-Order Concurrent Separation Logic