Daniel Gratzer

38 papers A* 4B 4Journal 29Unranked 1
YearRankTypeTitle / Venue / Authors
2026 J jnl
Normalization for multimodal type theory.
Log. Methods Comput. Sci.
Daniel Gratzer
2026 J jnl
The ∞-category of ∞categories in simplicial type theory.
CoRR
Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz
2025 J jnl
A Modal Deconstruction of Löb Induction.
Proc. ACM Program. Lang.
Daniel Gratzer
2025 J jnl
Controlling unfolding in type theory.
Math. Struct. Comput. Sci.
Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand, Lars Birkedal
2025 B conf
Idempotent Resources in Separation Logic - The Heart of core in Iris.
FoSSaCS
Daniel Gratzer, Mathias Adam Møller, Lars Birkedal
2025 A* conf
The Yoneda embedding in simplicial type theory.
LICS
Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz
2025 J jnl
The Yoneda embedding in simplicial type theory.
CoRR
Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz
2024 J jnl
Directed univalence in simplicial homotopy type theory.
CoRR
Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz
2024 J jnl
The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations.
CoRR
Daniel Gratzer, Håkon Robbestad Gylterud, Anders Mörtberg, Elisabeth Stenholm
2024 J jnl
The category of iterative sets in homotopy type theory and univalent foundations.
Math. Struct. Comput. Sci.
Daniel Gratzer, Håkon Robbestad Gylterud, Anders Mörtberg, Elisabeth Stenholm
2024 B conf
Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics.
CSL
Jonathan Sterling, Daniel Gratzer, Lars Birkedal
2024 J jnl
Unifying cubical and multimodal type theory.
Log. Methods Comput. Sci.
Frederik Lerbjerg Aagaard, Magnus Baunsgaard Kristensen, Daniel Gratzer, Lars Birkedal
2023 J jnl
Free theorems from univalent reference types.
CoRR
Jonathan Sterling, Daniel Gratzer, Lars Birkedal
2023 J jnl
Normalization for multimodal type theory.
CoRR
Daniel Gratzer
2023 J jnl
Under Lock and Key: a Proof System for a Multimodal Logic.
Bull. Symb. Log.
G. A. Kavvos, Daniel Gratzer
2022 J jnl
A Cubical Language for Bishop Sets.
Log. Methods Comput. Sci.
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
2022 B conf
A Stratified Approach to Löb Induction.
FSCD
Daniel Gratzer, Lars Birkedal
2022 J jnl
An inductive-recursive universe generic for small families.
CoRR
Daniel Gratzer
2022 J jnl
Controlling unfolding in type theory.
CoRR
Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand, Lars Birkedal
2022 J jnl
Denotational semantics of general store and polymorphism.
CoRR
Jonathan Sterling, Daniel Gratzer, Lars Birkedal
2022 J jnl
Modalities and Parametric Adjoints.
ACM Trans. Comput. Log.
Daniel Gratzer, Evan Cavallo, G. A. Kavvos, Adrien Guatto, Lars Birkedal
2022 A* conf
Normalization for Multimodal Type Theory.
LICS
Daniel Gratzer
2022 J jnl
Strict universes for Grothendieck topoi.
CoRR
Daniel Gratzer, Michael Shulman, Jonathan Sterling
2022 J jnl
The directed plump ordering.
CoRR
Daniel Gratzer, Michael Shulman, Jonathan Sterling
2022 J jnl
Under Lock and Key: A Proof System for a Multimodal Logic.
CoRR
G. A. Kavvos, Daniel Gratzer
2022 J jnl
Unifying cubical and multimodal type theory.
CoRR
Frederik Lerbjerg Aagaard, Magnus Baunsgaard Kristensen, Daniel Gratzer, Lars Birkedal
2022 — conf
{mitten}: A Flexible Multimodal Proof Assistant.
TYPES
Philipp Stassen, Daniel Gratzer, Lars Birkedal
2021 J jnl
Multimodal Dependent Type Theory.
Log. Methods Comput. Sci.
Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, Lars Birkedal
2021 J jnl
Normalization for multimodal type theory.
CoRR
Daniel Gratzer
2021 A* conf
Transfinite Iris: resolving an existential dilemma of step-indexed separation logic.
PLDI
Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, Lars Birkedal
2020 J jnl
A Cubical Language for Bishop Sets.
CoRR
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
2020 A* conf
Multimodal Dependent Type Theory.
LICS
Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, Lars Birkedal
2020 J jnl
Multimodal Dependent Type Theory.
CoRR
Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, Lars Birkedal
2020 J jnl
Syntactic categories for dependent type theory: sketching and adequacy.
CoRR
Daniel Gratzer, Jonathan Sterling
2019 B conf
Cubical Syntax for Reflection-Free Extensional Equality.
FSCD
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
2019 J jnl
Cubical Syntax for Reflection-Free Extensional Equality.
CoRR
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
2019 J jnl
Implementing a modal dependent type theory.
Proc. ACM Program. Lang.
Daniel Gratzer, Jonathan Sterling, Lars Birkedal
2019 J jnl
Iron: managing obligations in higher-order concurrent separation logic.
Proc. ACM Program. Lang.
Ales Bizjak, Daniel Gratzer, Robbert Krebbers, Lars Birkedal