A Sound and Complete Substitution Algorithm for Multimode Type Theory: Technical Report

TL;DR

This technical report provides a detailed, formal presentation of Well-Scoped Multimode Type Theory and proves the soundness and completeness of its substitution algorithm, enhancing the theoretical foundations of multimode type systems.

Contribution

It introduces a comprehensive formalization of Well-Scoped Multimode Type Theory and rigorously proves the soundness and completeness of its substitution algorithm.

Findings

Formal definition of WSMTT with detailed rules

Proofs of soundness and completeness of the substitution algorithm

Description of substitution-free multimode type theory

Abstract

This is the technical report accompanying the paper "A Sound and Complete Substitution Algorithm for Multimode Type Theory" [Ceulemans, Nuyts and Devriese, 2024]. It contains a full definition of Well-Scoped Multimode Type Theory (WSMTT) in Section 2, including many rules for $\sigma$-equivalence and a description of all rules that have been omitted. Furthermore, we present completeness and soundness proofs of the substitution algorithm in full detail. These can be found in Sections 4 and 5 respectively. In order to make this document relatively self-contained, we also include a description of Substitution-Free Multimode Type Theory (SFMTT) in Section 3.