Normalization for multimodal type theory

TL;DR

This paper establishes normalization for multimodal type theory (MTT) using a novel adaptation of Synthetic Tait Computability, leading to results on conversion, injectivity, and decidable type-checking.

Contribution

It introduces a new normalization proof for MTT by extending Synthetic Tait Computability to handle modalities and multiple modes.

Findings

Normalization of MTT proven using adapted Synthetic Tait Computability

Conversion problem reduced to mode theory's conversion problem

Type-checking is decidable when mode theory is decidable

Abstract

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 novel adaptation of Sterling's Synthetic Tait Computability which generalizes the framework to accommodate a type theory with modalities and multiple modes. As a corollary of our main result, we reduce the conversion problem of MTT to the conversion problem of its mode theory and show the injectivity of type constructors. Finally, we conclude that MTT enjoys decidable type-checking when instantiated with a decidable mode theory.