Subject Reduction vs Intersection / Union Types in λμμ

The role of Classical Logic in computer science is changing drastically over the last few years. Given the direct relation between the Lambda Calculus (Barendregt 1984) and intuitionistic logic, for many years it was believed that only the constructive logics had any real computational content, and only after Griffi n’s discovery of the relation between double-negation elimination (Griffi n 1990) and Felleisen’s control operators (Felleisen, Friedman, Kohlbecker, and Duba 1987) did the research community become aware of the computational advantages of Classical Logic. Since then, many researchers have focussed on different calculi, trying to exploit the Curry-Howard isomorphism for various classical logics, both in sequent style and in natural deduction, for computer science: amongst many, we mention (Parigot 1992; Ong and Stewart 1997; Curien and Herbelin 2000; Urban 2000; Wadler 2003). In this paper we contribute to that line of research by studying the λμμ -calculus (Curien and Herbelin 2000), which enjoys a Curry-Howard isomorphism for implicative G 3 (Kleene 1952), an variant of Gentzen’s system LK (Gentzen 1935).