Daniel Gratzer

List of research outcomes

This list is not complete and representing at the moment only items from zbMATH Open and arXiv. We are working on additional sources - please check back here soon!

Publication	Date of Publication	Type
Strict universes for Grothendieck topoi Theory and Applications of Categories	2026-06-08	Paper
Normalization for multimodal type theory Logical Methods in Computer Science	2026-03-23	Paper
Towards univalent reference types: the impact of univalence on denotational semantics	2026-02-19	Paper
Controlling unfolding in type theory Mathematical Structures in Computer Science	2025-12-30	Paper
Idempotent resources in separation logic. The heart of \texttt{core} in Iris	2025-12-04	Paper
The category of iterative sets in homotopy type theory and univalent foundations Mathematical Structures in Computer Science	2025-03-04	Paper
Unifying cubical and multimodal type theory Logical Methods in Computer Science	2025-01-31	Paper
Normalization for multimodal type theory	2024-12-06	Paper
{mitten}: a flexible multimodal proof assistant	2024-11-26	Paper
A stratified approach to Löb induction	2024-05-27	Paper
UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC The Bulletin of Symbolic Logic	2023-08-10	Paper
scientific article; zbMATH DE number 7566056 (Why is no real title available?) (available as arXiv preprint)	2022-08-02	Paper
scientific article; zbMATH DE number 7566056 (Why is no real title available?)	2022-08-02	Paper
scientific article; zbMATH DE number 7559297 (Why is no real title available?) (available as arXiv preprint)	2022-07-18	Paper
Modalities and Parametric Adjoints ACM Transactions on Computational Logic	2022-04-29	Paper
Strict universes for Grothendieck topoi	2022-02-24	Paper
The directed plump ordering	2022-02-15	Paper
Multimodal dependent type theory (available as arXiv preprint)	2021-10-08	Paper
Multimodal dependent type theory	2021-10-08	Paper
Multimodal dependent type theory Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science	2021-01-21	Paper
A Cubical Language for Bishop Sets (available as arXiv preprint)	2020-03-03	Paper
Cubical Syntax for Reflection-Free Extensional Equality (available as arXiv preprint)	2019-04-17	Paper
The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations (available as arXiv preprint)	N/A	Paper

Research outcomes over time

This page was built for person: Daniel Gratzer