Daniel Gratzer

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)