Daniel Gratzer

Normalization for multimodal type theory

2021 · arXiv (Cornell University)

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 …