A Sound and Complete Substitution Algorithm for Multimode Type Theory: Technical Report
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909227948179456 |
|---|---|
| author | Ceulemans, Joris Nuyts, Andreas Devriese, Dominique |
| author_facet | Ceulemans, Joris Nuyts, Andreas Devriese, Dominique |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2406_13622 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | A Sound and Complete Substitution Algorithm for Multimode Type Theory: Technical Report Ceulemans, Joris Nuyts, Andreas Devriese, Dominique 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 $σ$-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. |
| title | A Sound and Complete Substitution Algorithm for Multimode Type Theory: Technical Report |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2406.13622 |