Strong normalization through idempotent intersection types: a new syntactical approach

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 r…