19 citations · 47 across the 12 of their papers we have counts for
Showing 2023Show all
2 papers · 1 filter
cs.LO2023
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…
cs.LO2023★ 1 cited
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…