多模态类型论的可靠且完备替换算法：技术报告
A Sound and Complete Substitution Algorithm for Multimode Type Theory: Technical Report
AI总结：
该技术报告配套多模态类型论替换算法相关论文，给出WSMTT完整定义、替换算法的可靠性与完备性详细证明，还补充SFMTT说明以保证文档自包含。
摘要：
本技术报告配套论文《多模态类型论的可靠且完备替换算法》[Ceulemans、Nuyts 与 Devriese，2024]。第2节给出了良界多模态类型论（WSMTT）的完整定义，包含σ等价的诸多规则，以及所有被省略规则的说明。此外，我们完整详细地呈现了替换算法的完备性与可靠性证明，分别位于第4节和第5节。为使本文档相对自包含，我们还在第3节介绍了无替换多模态类型论（SFMTT）。
英文摘要：
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 $σ$-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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
