D. Gratzer
Conditionally accepted to Principles of Programming Languages
2025
- A modal deconstruction of Löb induction
- 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 2024 - 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