A Translation of Intersection and Union Types for the λμ-Calculus

Abstract

We introduce an intersection and union type system for the λμ-calculus, which includes a restricted version of the traditional union-elimination rule. We give a translation from intersection and union types into intersection and product types, which is a variant of negative translation from classical logic to intuitionistic logic and naturally reflects the structure of strict intersection and union types. It is shown that a derivation in our type system can be translated into a derivation in the type system of van Bakel, Barbanera and de’Liguoro. As a corollary, the terms typable in our system turn out to be strongly normalising. We also present an intersection and union type system in the style of sequent calculus, and show that the terms typable in the system coincide with the strongly normalising terms of the $\overline\lambda$ μ-calculus, a call-by-name fragment of Curien and Herbelin’s $\overline\lambda\mu\widetilde{\mu}$-calculus.