Intersection and Union Types in the λ¯μμ˜-calculus

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.