Cubical Syntax for Reflection-Free Extensional Equality. - Jonathan Sterling; Carlo Angiuli; Daniel Gratzer (FSCD, 2019)

Iron: managing obligations in higher-order concurrent separation logic. - Ales Bizjak; Daniel Gratzer; Robbert Krebbers; Lars Birkedal (Proc. ACM Program. Lang., 2019)

Implementing a modal dependent type theory. - Daniel Gratzer; Jonathan Sterling; Lars Birkedal (Proc. ACM Program. Lang., 2019)

Syntactic categories for dependent type theory: sketching and adequacy. - Daniel Gratzer; Jonathan Sterling (CoRR, 2020)

Transfinite Iris: resolving an existential dilemma of step-indexed separation logic. - Simon Spies; Lennard Gäher; Daniel Gratzer; Joseph Tassarotti; Robbert Krebbers; Derek Dreyer; Lars Birkedal (PLDI, 2021)

Multimodal Dependent Type Theory. - Daniel Gratzer; G. A. Kavvos; Andreas Nuyts; Lars Birkedal (Log. Methods Comput. Sci., 2021)

A Stratified Approach to Löb Induction. - Daniel Gratzer; Lars Birkedal (FSCD, 2022)

Normalization for Multimodal Type Theory. - Daniel Gratzer (LICS, 2022)

{mitten}: A Flexible Multimodal Proof Assistant. - Philipp Stassen; Daniel Gratzer; Lars Birkedal (TYPES, 2022)

An inductive-recursive universe generic for small families. - Daniel Gratzer (CoRR, 2022)

The directed plump ordering. - Daniel Gratzer; Michael Shulman; Jonathan Sterling (CoRR, 2022)

Strict universes for Grothendieck topoi. - Daniel Gratzer; Michael Shulman; Jonathan Sterling (CoRR, 2022)

Denotational semantics of general store and polymorphism. - Jonathan Sterling; Daniel Gratzer; Lars Birkedal (CoRR, 2022)

Controlling unfolding in type theory. - Daniel Gratzer; Jonathan Sterling; Carlo Angiuli; Thierry Coquand; Lars Birkedal (CoRR, 2022)

A Cubical Language for Bishop Sets. - Jonathan Sterling; Carlo Angiuli; Daniel Gratzer (Log. Methods Comput. Sci., 2022)

Modalities and Parametric Adjoints. - Daniel Gratzer; Evan Cavallo; G. A. Kavvos; Adrien Guatto; Lars Birkedal (ACM Trans. Comput. Log., 2022)

Free theorems from univalent reference types. - Jonathan Sterling; Daniel Gratzer; Lars Birkedal (CoRR, 2023)

Under Lock and Key: a Proof System for a Multimodal Logic. - G. A. Kavvos; Daniel Gratzer (Bull. Symb. Log., 2023)

Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics. - Jonathan Sterling; Daniel Gratzer; Lars Birkedal (CSL, 2024)

Directed univalence in simplicial homotopy type theory. - Daniel Gratzer; Jonathan Weinberger; Ulrik Buchholtz (CoRR, 2024)

Unifying cubical and multimodal type theory. - Frederik Lerbjerg Aagaard; Magnus Baunsgaard Kristensen; Daniel Gratzer; Lars Birkedal (Log. Methods Comput. Sci., 2024)

The category of iterative sets in homotopy type theory and univalent foundations. - Daniel Gratzer; Håkon Robbestad Gylterud; Anders Mörtberg; Elisabeth Stenholm (Math. Struct. Comput. Sci., 2024)

Idempotent Resources in Separation Logic - The Heart of core in Iris. - Daniel Gratzer; Mathias Adam Møller; Lars Birkedal (FoSSaCS, 2025)

A Modal Deconstruction of Löb Induction. - Daniel Gratzer (Proc. ACM Program. Lang., 2025)

The Yoneda embedding in simplicial type theory. - Daniel Gratzer; Jonathan Weinberger; Ulrik Buchholtz (CoRR, 2025)