Paper: Separation with Streams in the ?µ-calculus (at LICS 2005)
Authors: Alexis SaurinAbstract
The ??-calculus is an extension of the ?-calculus introduced in 1992 by Parigot [17] 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 [5] proved that the Separation Property (also referred to as Böhm theorem) fails for Parigot's ??-calculus. By analyzing David and 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 and Py.
BibTeX
@InProceedings{Saurin-SeparationwithStrea, author = {Alexis Saurin}, title = {Separation with Streams in the ?µ-calculus}, booktitle = {Proceedings of the Twentieth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2005}, year = 2005, editor = {Prakash Panangaden}, month = {June}, pages = {356--365}, location = {Chicago, USA}, publisher = {IEEE Computer Society Press} }