A Sound and Complete Substitution Algorithm for Multimode Type Theory: Technical Report
<|reference_start|>A Sound and Complete Substitution Algorithm for Multimode Type Theory: Technical Report: 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.<|reference_end|>
@article{ceulemans2024a,
    title={A Sound and Complete Substitution Algorithm for Multimode Type Theory:
  Technical Report},
    author={Joris Ceulemans (KU Leuven), Andreas Nuyts (KU Leuven), Dominique
  Devriese (KU Leuven)},
    journal={arXiv preprint arXiv:2406.13622},
    year={2024},
    archivePrefix={arXiv},
    eprint={2406.13622},
    primaryClass={cs.LO}
}