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