I am a Ph.D. student in the Department of Computer Science at Aarhus University. I am advised by Lars Birkedal.
I study programming languages, type theories, and logics. I am particularly interested in applying semantic methods to prove syntactic properties of modal type theories and programming languages. I am also involved in the development of program logics for concurrent programming languages through the Iris project.
Teaching
 Teaching assistant under Amin Timany and Jean Pichon for the Fall 2022 iteration of Compilers
 Coorganizer with Lars Birkedal of the Spring 2021 iteration of Categorical Type Theory.
 Teaching assistant under Lars Birkedal for the Fall 2020 iteration of Category Theory
 Teaching assistant under Lars Birkedal and Anders Møller for the Fall 2019 iteration of Program Analysis and Verification
Publications
Please see my bibliography for bibtex entries for my published papers.
Under Lock and Key: A Proof System for a Multimodal Logic
G. A. Kavvos, D. Gratzer
The Bulletin of Symbolic Logic, 2023
(Arxiv, PDF) 
mitten: flexible multimodal proof assistant
P. Stassen, D. Gratzer, L. Birkedal
TYPES 2022 Postproceedings, 2023
(PDF) 
A stratified approach to Löb induction
D. Gratzer, L. Birkedal
Formal Structures for Computation and Deduction, 2022
(PDF, Errata, Slides) 
Normalization for multimodal type theory
D. Gratzer
Logic in Computer Science, 2022
(PDF, Short abstract, Long article, Arxiv, Slides)

A Cubical Language for Bishop Sets
J. Sterling, C. Angiuli, and D. Gratzer
Logical Methods in Computer Science, 2022
(PDF, Arxiv) 
Modalities and Parametric Adjoints
D. Gratzer, E. Cavallo, G.A. Kavvos, A. Guatto, L. Birkedal
Transactions on Computational Logic, 2022
(PDF, Short abstract)

Multimodal Dependent Type Theory
D. Gratzer, G. A. Kavvos, A. Nuyts, and L. Birkedal
Logic Methods in Computer Science, 2021
(PDF, Arxiv) 
Transfinite Iris: Resolving an Existential Dilemma of StepIndexed Separation Logic
S. Spies, L. Gäher, D. Gratzer, J. Tassarotti, R. Krebbers, D. Dreyer, L. Birkedal
Programming Language Design and Implementation, 2021
(PDF, Appendix, Coq Development) 
Multimodal Dependent Type Theory
D. Gratzer, G. A. Kavvos, A. Nuyts, and L. Birkedal
Logic in Computer Science, 2020
(PDF, Technical Report) 
Implementing a Modal Dependent Type Theory
D. Gratzer, J. Sterling, and L. Birkedal
International Conference on Functional Programming, 2019
(PDF, Technical Report, Experimental Implementation, Slides)
Distinguished Paper at ICFP'19 
Cubical Syntax for ReflectionFree Extensional Equality
J. Sterling, C. Angiuli, and D. Gratzer
Formal Structures for Computation and Deduction, 2019
(PDF, Extended Arxiv Version)
Best Paper Award for Junior Researchers 
Iron: Managing Obligations in HigherOrder Concurrent Separation Logic
A. Bizjak, D. Gratzer, R. Krebbers, and L. Birkedal.
Principles of Programming Languages, 2019.
(PDF, Website, Coq Development)
Selected Preprints and Unpublished Notes

Syntax and semantics of modal type theory
D. Gratzer
Submitted draft of my PhD thesis
(PDF) 
Free theorems from univalent reference types
J. Sterling, D. Gratzer, L. Birkedal
2023
(Arxiv, PDF) 
Adjoint modalities in MTT
D. Gratzer
2023
(PDF)

Controlling unfolding in type theory
D. Gratzer, J. Sterling, C. Angiuli, T. Coquand, L. Birkedal
2022
(PDF) 
Denotational semantics of general store and polymorphism
J. Sterling, D. Gratzer, L. Birkedal
2022
(Arxiv, PDF) 
Unifying cubical and multimodal type theory
F. Lerbjerg Aagaard, M. Baunsgaard Kristensen, D. Gratzer, L. Birkedal
2022
(Arxiv, PDF) 
Strict universes for Grothendieck topoi
D. Gratzer, M. Shulman, and J. Sterling
2022
(Arxiv, PDF) 
The directed plump ordering
D. Gratzer, M. Shulman, and J. Sterling
2022
(Arxiv, PDF) 
An inductiverecursive universe generic for small families
D. Gratzer
2022
(Arxiv, PDF) 
Crisp induction for intensional identity types
D. Gratzer
2021
(PDF)

Syntactic categories for dependent type theory: sketching and adequacy
D. Gratzer, J. Sterling
2020
(PDF, Arxiv)

An Addendum to Section 7 of First Steps in Synthetic Guarded Domain Theory
D. Gratzer
2018
(PDF, Github Repo) 
Formalizing Concurrent Stacks With Helping: A Case Study In Iris
D. Gratzer, M. Høier, A. Bizjak, and L. Birkedal
2017.
(PDF, Coq Development)
The Coq source has been updated and revised 
On the Independence of The Continuum Hypothesis
D. Gratzer
2017
(PDF, Github Repo)
Selected Talks

Controlling unfolding in type theory
D. Gratzer, J. Sterling. C. Angiuli, T. Coquand, L. Birkedal
WG 6 meeting, 2023
(Slides) 
Modalities and (weak) dependent right adjoints
D. Gratzer
HoTTEST, 2023
(Slides, Recording) 
Denotational semantics of type theory
D. Gratzer
LogSem Seminar, 2023
(Speaker notes) 
Normalization for multimodal type theory
D. Gratzer
TYPES, 2021
(Slides, Recording) 
Modalities and Parametric Adjoints
D. Gratzer, E. Cavallo, G.A. Kavvos, A. Guatto, L. Birkedal
TYPES, 2021
(Slides, Recording) 
Multimodal Dependent Type Theory
D. Gratzer, G.A. Kavvos, A. Nuyts, and L. Birkedal
Stockholm University, Logic Seminar, 2020
(Slides) 
Multimodal Dependent Type Theory
D. Gratzer, G.A. Kavvos, A. Nuyts, and L. Birkedal
IT University of Copenhagen, PLZ Seminar, 2020
(Slides) 
Implementing a Modal Dependent Type Theory
D. Gratzer, J. Sterling, and L. Birkedal
International Conference on Functional Programming, 2019
(Slides) 
Implementing Type Theory
D. Gratzer
Computer Science Day (Aarhus University), 2019.
(Slides) 
Iron: Managing Obligations in HigherOrder Concurrent Separation Logic
A. Bizjak, D. Gratzer, R. Krebbers, and L. Birkedal.
Principles of Programming Languages, 2019.
(Slides) 
An Introduction to NormalizationbyEvaluation
D. Gratzer.
Aarhus LogSem Seminar, 2018.
(Slides)