Daniel Gratzer

Publication Activity (10 Years)

Years Active: 2019-2024
Publications (10 Years): 29

Top Topics

Theoretical Basis

Syntactic Categories

Top Venues

Proc. ACM Program. Lang.

Publications

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