Normalization for multimodal type theory
This provides a foundational result for researchers in type theory and formal verification, enabling reliable type checking in modal contexts, though it is incremental as it extends existing synthetic Tait computability methods.
The paper tackles the problem of proving normalization for MTT, a multimodal dependent type theory, and shows that type checking and conversion can be reduced to deciding modality equality, yielding a type checking algorithm for all known instantiations.
We prove normalization for MTT, a general multimodal dependent type theory capable of expressing modal type theories for guarded recursion, internalized parametricity, and various other prototypical modal situations. We prove that deciding type checking and conversion in MTT can be reduced to deciding the equality of modalities in the underlying modal situation, immediately yielding a type checking algorithm for all instantiations of MTT in the literature. This proof uses a generalization of synthetic Tait computability -- an abstract approach to gluing proofs -- to account for modalities. This extension is based on MTT itself, so that this proof also constitutes a significant case study of MTT.