# zbMATH — the first resource for mathematics

Intersection and union types in the $$\bar{\lambda}\mu\tilde{\mu}$$-calculus. (English) Zbl 1272.03078
Coppo, Mario (ed.) et al., Proceedings of the 3rd international workshop on intersection types and related systems (ITRS 2004), Turku, Finland, July 13, 2004. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 136, 153-172 (2005).
Summary: The original $$\bar{\lambda}\mu\tilde{\mu}$$ 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 $$\bar{\lambda}\mu\tilde{\mu}$$ with intersection and union types. The intrinsic symmetry in the $$\bar{\lambda}\mu\tilde{\mu}$$ calculus leads to an essential use of both intersection and union types.
For the entire collection see [Zbl 1272.68014].

##### MSC:
 03B40 Combinatory logic and lambda calculus
Full Text: