On the Formal Metatheory of the Pure Type Systems using One-sorted Variable Names and Multiple Substitutions
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866918160248078336 |
|---|---|
| author | Urciuoli, Sebastián |
| author_facet | Urciuoli, Sebastián |
| contents | We develop formal theories of conversion for Church-style lambda-terms with Pi-types in first-order syntax using one-sorted variables names and Stoughton's multiple substitutions. We then formalize the Pure Type Systems along some fundamental metatheoretic properties: weakening, syntactic validity, closure under alpha-conversion and substitution. Finally, we compare our formalization with others related. The whole development has been machine-checked using the Agda system. Our work demonstrates that the mechanization of dependent type theory by using conventional syntax and without identifying alpha-convertible lambda-terms is feasible. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2510_12300 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | On the Formal Metatheory of the Pure Type Systems using One-sorted Variable Names and Multiple Substitutions Urciuoli, Sebastián Logic in Computer Science F.4.1 We develop formal theories of conversion for Church-style lambda-terms with Pi-types in first-order syntax using one-sorted variables names and Stoughton's multiple substitutions. We then formalize the Pure Type Systems along some fundamental metatheoretic properties: weakening, syntactic validity, closure under alpha-conversion and substitution. Finally, we compare our formalization with others related. The whole development has been machine-checked using the Agda system. Our work demonstrates that the mechanization of dependent type theory by using conventional syntax and without identifying alpha-convertible lambda-terms is feasible. |
| title | On the Formal Metatheory of the Pure Type Systems using One-sorted Variable Names and Multiple Substitutions |
| topic | Logic in Computer Science F.4.1 |
| url | https://arxiv.org/abs/2510.12300 |