Normalization for multimodal type theory

06/02/2021
by   Daniel Gratzer, et al.
0

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.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset