3 papers
cs.LO2026
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…
cs.LO2025
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…
cs.LO2024
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…