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.

翻译：众所周知，交集类型指派系统可用于刻画强规范化性质。这类系统中可类型化λ项具有强规范性的典型证明通常依赖于语义学技术。本文研究$Λ_\cap^e$——这是Coppo与Dezani（柯里风格）交集类型系统的一个变体，并提出其强规范性的语法证明。我们首先设计$Λ_\cap^i$作为其丘奇风格版本，其中项与类型推导过程严格对应。随后通过构造度量函数证明$Λ_\cap^i$的可类型化蕴含强规范化：该函数对任意给定项生成自然数，该数值随归约过程严格递减。最终，由于两个系统可相互模拟，该结论被推广至$Λ_\cap^e$系统。