19 citations · 47 across the 12 of their papers we have counts for
14 papers
Towards univalent reference types
Jonathan Sterling, Daniel Gratzer, Lars Birkedal
We develop a denotational semantics for general reference types in an impredicative version of guarded homotopy type theory, an adaptation of synthetic guarded domain theory to Voe…
Normalization for multimodal type theory
Daniel Gratzer
We prove normalization for MTT, a general multimodal dependent type theory capable of expressing modal type theories for guarded recursion, internalized parametricity, and various…
Under Lock and Key: A Proof System for a Multimodal Logic
G. A. Kavvos, Daniel Gratzer
We present a proof system for a multimodal logic, based on our previous work on a multimodal Martin-Loef type theory. The specification of modes, modalities, and implications betwe…
Controlling unfolding in type theory
Daniel Gratzer, Jonathan Sterling, Carlo Angiuli +2
We present a new way to control the unfolding of definitions in dependent type theory. Traditionally, proof assistants require users to fix whether each definition will or will not…
Denotational semantics of general store and polymorphism
Jonathan Sterling, Daniel Gratzer, Lars Birkedal
We contribute the first denotational semantics of polymorphic dependent type theory extended by an equational theory for general (higher-order) reference types and recursive types,…
The directed plump ordering
Daniel Gratzer, Michael Shulman, Jonathan Sterling
Based on Taylor's hereditarily directed plump ordinals, we define the directed plump ordering on W-types in Martin-Löf type theory. This ordering is similar to the plump ordering b…
Unifying cubical and multimodal type theory
Frederik Lerbjerg Aagaard, Magnus Baunsgaard Kristensen, Daniel Gratzer +1
In this paper we combine the principled approach to modalities from multimodal type theory (MTT) with the computationally well-behaved realization of identity types from cubical ty…
An inductive-recursive universe generic for small families
Daniel Gratzer
We show that it is possible to construct a universe in all Grothendieck topoi with injective codes a la Pujet and Tabareau which is nonetheless generic for small families. As a tri…
Strict universes for Grothendieck topoi
Daniel Gratzer, Michael Shulman, Jonathan Sterling
Hofmann and Streicher famously showed how to lift Grothendieck universes into presheaf topoi, and Streicher has extended their result to the case of sheaf topoi by sheafification.…
Normalization for multimodal type theory
Daniel Gratzer
We consider the conversion problem for multimodal type theory (MTT) by characterizing the normal forms of the type theory and proving normalization. Normalization follows from a no…
Syntactic categories for dependent type theory: sketching and adequacy
Daniel Gratzer, Jonathan Sterling
We argue that locally Cartesian closed categories form a suitable doctrine for defining dependent type theories, including non-extensional ones. Using the theory of sketches, one m…
Multimodal Dependent Type Theory
Daniel Gratzer, G. A. Kavvos, Andreas Nuyts +1
We introduce MTT, a dependent type theory which supports multiple modalities. MTT is parametrized by a mode theory which specifies a collection of modes, modalities, and transforma…
A Cubical Language for Bishop Sets
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
We present XTT, a version of Cartesian cubical type theory specialized for Bishop sets à la Coquand, in which every type enjoys a definitional version of the uniqueness of identity…
Cubical Syntax for Reflection-Free Extensional Equality
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
We contribute XTT, a cubical reconstruction of Observational Type Theory which extends Martin-Löf's intensional type theory with a dependent equality type that enjoys function exte…