Tags:lambda calculus, simple types and uniform intersection types

Abstract:

A new proof of strong normalization for simple type assignment for λ-calculus is obtained, through a translation from this system to a system of uniform intersection types, which is equivalent to it as typability power and whose strong normalization property can be easily proved by induction on derivation.

Strong normalization of simple types through uniform intersection types.