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 $\Lambda_\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 $\Lambda_\cap^i$, a Church-style version, in which terms closely correspond to typing derivations. Then we prove that typability in $\Lambda_\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 $\Lambda_\cap^e$, since the two systems simulate each other.

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