I am a postdoctoral researcher in the Department of Computer Science at Aarhus University under Lars Birkedal. I am presently at Oxford University as a visiting researcher.
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.
Carlo Angiuli and I are currently working on a book on dependent type theory. An early draft of the manuscript is available here: Principles of Dependent Type Theory
Teaching
- Co-lecturer with Lars Birkedal for the Spring 2024 iteration of Modern Dependent Type Theory
- Teaching assistant under Amin Timany and Jean Pichon for the Fall 2022 iteration of Compilers
- Co-organizer 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.-
Free theorems from univalent reference types
J. Sterling, D. Gratzer, L. Birkedal
Computer Science Logic, 2024
(Arxiv, PDF) -
Syntax and semantics of modal type theory
D. Gratzer
PhD thesis
(PDF) -
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 Post-proceedings, 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 Step-Indexed 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 Reflection-Free 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 Higher-Order 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
-
Directed univalence in simplicial homotopy type theory
D. Gratzer, J. Weinberger, U. Buchholtz
2024
(PDF) -
The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations
D. Gratzer, H. Gylterud, A. Mörtberg, E. Stenholm
2024
(PDF, Arxiv) -
A modal deconstruction of Löb induction
D. Gratzer
2024
(PDF)
-
Weak-head conversion testing for MTT
D. Gratzer
2023
(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 inductive-recursive 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 Higher-Order Concurrent Separation Logic
A. Bizjak, D. Gratzer, R. Krebbers, and L. Birkedal.
Principles of Programming Languages, 2019.
(Slides) -
An Introduction to Normalization-by-Evaluation
D. Gratzer.
Aarhus LogSem Seminar, 2018.
(Slides)