A Translation of Intersection and Union Types for the lambda-mu Calculus

ABSTRACT. We introduce an intersection and union type system for the lambda-mu calculus, which includes a restricted version of the traditional union-elimination rule. Strong normalisation of terms typable by the system is shown via a translation of intersection and union types into intersection and product types, relying on the result of strong normalisation of terms typable by van Bakel, Barbanera and de'Liguoro's system.