Paper: Separation with Streams in the lambdaµ-calculus (at LICS 2005)

Authors: Alexis Saurin

Abstract

The lambdamu-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 lambdaµ-calculus},
    booktitle =  {Proceedings of the Twentieth Annual IEEE Symposium on Logic in Computer Science (LICS 2005)},
    year =	 {2005},
    month =	 {June}, 
    pages =      {356--365},
    location =   {Chicago, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }