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].

03B40 Combinatory logic and lambda calculus
Full Text: Link