Daniel Gratzer

According to our database, Daniel Gratzer authored at least 21 papers between 2019 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations.

Daniel Gratzer, Håkon Gylterud, Anders Mörtberg, Elisabeth Stenholm

CoRR, 2024

Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics.

Jonathan Sterling, Daniel Gratzer, Lars Birkedal

Proceedings of the 32nd EACSL Annual Conference on Computer Science Logic, 2024

2023

Under Lock and Key: a Proof System for a Multimodal Logic.

G. A. Kavvos, Daniel Gratzer

Bull. Symb. Log., June, 2023

Free theorems from univalent reference types.

Jonathan Sterling, Daniel Gratzer, Lars Birkedal

CoRR, 2023

2022

Modalities and Parametric Adjoints.

Daniel Gratzer, Evan Cavallo, G. A. Kavvos, Adrien Guatto, Lars Birkedal

ACM Trans. Comput. Log., 2022

A Cubical Language for Bishop Sets.

Jonathan Sterling, Carlo Angiuli, Daniel Gratzer

Log. Methods Comput. Sci., 2022

Controlling unfolding in type theory.

Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand, Lars Birkedal

CoRR, 2022

Denotational semantics of general store and polymorphism.

Jonathan Sterling, Daniel Gratzer, Lars Birkedal

CoRR, 2022

Unifying cubical and multimodal type theory.

Frederik Lerbjerg Aagaard, Magnus Baunsgaard Kristensen, Daniel Gratzer, Lars Birkedal

CoRR, 2022

Strict universes for Grothendieck topoi.

Daniel Gratzer, Michael Shulman, Jonathan Sterling

CoRR, 2022

The directed plump ordering.

Daniel Gratzer, Michael Shulman, Jonathan Sterling

CoRR, 2022

An inductive-recursive universe generic for small families.

Daniel Gratzer

CoRR, 2022

{mitten}: A Flexible Multimodal Proof Assistant.

Philipp Stassen, Daniel Gratzer, Lars Birkedal

Proceedings of the 28th International Conference on Types for Proofs and Programs, 2022

Normalization for Multimodal Type Theory.

Daniel Gratzer

Proceedings of the LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2, 2022

A Stratified Approach to Löb Induction.

Daniel Gratzer, Lars Birkedal

Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction, 2022

2021

Multimodal Dependent Type Theory.

Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, Lars Birkedal

Log. Methods Comput. Sci., 2021

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

Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

2020

Syntactic categories for dependent type theory: sketching and adequacy.

Daniel Gratzer, Jonathan Sterling

CoRR, 2020

2019

Implementing a modal dependent type theory.

Daniel Gratzer, Jonathan Sterling, Lars Birkedal

Proc. ACM Program. Lang., 2019

Iron: managing obligations in higher-order concurrent separation logic.

Ales Bizjak, Daniel Gratzer, Robbert Krebbers, Lars Birkedal

Proc. ACM Program. Lang., 2019

Cubical Syntax for Reflection-Free Extensional Equality.

Jonathan Sterling, Carlo Angiuli, Daniel Gratzer

Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction, 2019