تقرير
A Sound and Complete Substitution Algorithm for Multimode Type Theory: Technical Report
| العنوان: | A Sound and Complete Substitution Algorithm for Multimode Type Theory: Technical Report |
|---|---|
| المؤلفون: | Ceulemans, Joris, Nuyts, Andreas, Devriese, Dominique |
| سنة النشر: | 2024 |
| المجموعة: | Computer Science |
| مصطلحات موضوعية: | Computer Science - Logic in Computer Science |
| الوصف: | 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. Comment: 36 pages, 10 figures |
| نوع الوثيقة: | Working Paper |
| URL الوصول: | http://arxiv.org/abs/2406.13622 |
| رقم الأكسشن: | edsarx.2406.13622 |
| قاعدة البيانات: | arXiv |
| الوصف غير متاح. |