Daniel Gratzer

Orcid: 0000-0003-1944-0789

According to our database1, Daniel Gratzer authored at least 22 papers between 2019 and 2024.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Directed univalence in simplicial homotopy type theory.
CoRR, 2024

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

Towards Univalent Reference Types: The Impact of Univalence on Denotational Semantics.
Proceedings of the 32nd EACSL Annual Conference on Computer Science Logic, 2024

2023
Under Lock and Key: a Proof System for a Multimodal Logic.
Bull. Symb. Log., June, 2023

Free theorems from univalent reference types.
CoRR, 2023

2022
Modalities and Parametric Adjoints.
ACM Trans. Comput. Log., 2022

A Cubical Language for Bishop Sets.
Log. Methods Comput. Sci., 2022

Controlling unfolding in type theory.
CoRR, 2022

Denotational semantics of general store and polymorphism.
CoRR, 2022

Unifying cubical and multimodal type theory.
CoRR, 2022

Strict universes for Grothendieck topoi.
CoRR, 2022

The directed plump ordering.
CoRR, 2022

An inductive-recursive universe generic for small families.
CoRR, 2022

{mitten}: A Flexible Multimodal Proof Assistant.
Proceedings of the 28th International Conference on Types for Proofs and Programs, 2022

Normalization for Multimodal Type Theory.
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.
Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction, 2022

2021
Multimodal Dependent Type Theory.
Log. Methods Comput. Sci., 2021

Transfinite Iris: resolving an existential dilemma of step-indexed separation logic.
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.
CoRR, 2020

2019
Implementing a modal dependent type theory.
Proc. ACM Program. Lang., 2019

Iron: managing obligations in higher-order concurrent separation logic.
Proc. ACM Program. Lang., 2019

Cubical Syntax for Reflection-Free Extensional Equality.
Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction, 2019


  Loading...