Separation with streams in the Λμ-calculus

The λμ-calculus is an extension of the λ-calculus introduced in 1992 by Parigot (M. Parigot, 1992) in order to generalize the Curry-Howard isomorphism to classical logic. Two versions of the calculus are usually considered in the literature: Parigot´s original syntax and an alternative syntax introduced by de Groote. In 2001, David and Py (R. David, 2001) proved that the Separation Property (also referred to as Bohm theorem) fails for Parigot´s λμ-calculus. By analyzing David & Py´s result, we exhibit an extension of Parigot´s λμ-calculus, the Λμ-calculus, for which the Separation Property holds and which is built as an intermediate language between Parigot´s and de Groote´s λμ-calculi. We prove the theorem and describe how Λμ-calculus can be considered as a calculus of terms and streams. We then illustrate Separation in showing how in Λμ-calculus it is possible to separate the counter-example used by David & Py.