Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | https://arxiv.org/abs/2503.09831 |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866914358064316416 |
|---|---|
| author | Barenbaum, Pablo Della Rocca, Simona Ronchi Sottile, Cristian |
| author_facet | Barenbaum, Pablo Della Rocca, Simona Ronchi Sottile, Cristian |
| contents | It is well-known that intersection type assignment systems can be used to characterize strong normalization (SN). Typical proofs that typable lambda-terms are SN in these systems rely on semantical techniques. In this work, we study $Λ_\cap^e$, a variant of Coppo and Dezani's (Curry-style) intersection type system, and we propose a syntactical proof of strong normalization for it. We first design $Λ_\cap^i$, a Church-style version, in which terms closely correspond to typing derivations. Then we prove that typability in $Λ_\cap^i$ implies SN through a measure that, given a term, produces a natural number that decreases along with reduction. Finally, the result is extended to $Λ_\cap^e$, since the two systems simulate each other. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2503_09831 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Strong normalization through idempotent intersection types: a new syntactical approach Barenbaum, Pablo Della Rocca, Simona Ronchi Sottile, Cristian Logic in Computer Science It is well-known that intersection type assignment systems can be used to characterize strong normalization (SN). Typical proofs that typable lambda-terms are SN in these systems rely on semantical techniques. In this work, we study $Λ_\cap^e$, a variant of Coppo and Dezani's (Curry-style) intersection type system, and we propose a syntactical proof of strong normalization for it. We first design $Λ_\cap^i$, a Church-style version, in which terms closely correspond to typing derivations. Then we prove that typability in $Λ_\cap^i$ implies SN through a measure that, given a term, produces a natural number that decreases along with reduction. Finally, the result is extended to $Λ_\cap^e$, since the two systems simulate each other. |
| title | Strong normalization through idempotent intersection types: a new syntactical approach |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2503.09831 |