Intersection and union types in the λ̄μμ̃-calculus

Abstract

The original λ̄μμ̃ of Curien and Herbelin has a system of simple types, based on sequent calculus, embodying a Curry-Howard correspondence with classical logic. We introduce and discuss three type assignment systems that are extensions of λ̄μμ̃ with intersection and union types. The intrinsic symmetry in the λ̄μ μ̃ calculus leads to an essential use of both intersection and union types.