Normalization for multimodal type theory

TL;DR

This paper proves normalization for a comprehensive multimodal dependent type theory, enabling effective type checking across various modal systems through a generalized synthetic Tait computability approach.

Contribution

It introduces a normalization proof for MTT, a versatile multimodal dependent type theory, and develops a modal-aware synthetic Tait computability method.

Findings

Type checking reduces to modal equality decision

Provides a universal type checking algorithm for MTT variants

Demonstrates the approach as a case study of MTT

Abstract

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.