Pablo Barenbaum ; Simona Ronchi Della Rocca ; Cristian Sottile - Strong normalization through idempotent intersection types: a new syntactical approach

entics:16693 - Electronic Notes in Theoretical Informatics and Computer Science, December 20, 2025, Volume 5 - Proceedings of MFPS XLI - https://doi.org/10.46298/entics.16693
Strong normalization through idempotent intersection types: a new syntactical approachArticle

Authors: Pablo Barenbaum ; Simona Ronchi Della Rocca ; Cristian Sottile

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.


Volume: Volume 5 - Proceedings of MFPS XLI
Published on: December 20, 2025
Accepted on: October 15, 2025
Submitted on: April 3, 2025
Keywords: Logic in Computer Science

Consultation statistics

This page has been seen 221 times.
This article's PDF has been downloaded 75 times.