Logic in Computer Science (LICS 1992)

Paper: The lazy lambda calculus in a concurrency scenario (at LICS 1992)

Authors: Sangiorgi, D.

Abstract

The use of lambda calculus in richer settings, possibly involving parallelism, is examined in terms of its effect on the equivalence between lambda terms, focusing on S. Abramsky's (Ph.D thesis, Univ. of London, 1987) lazy lambda calculus. First, the lambda calculus is studied within a process calculus by examining the equivalence induced by R. Milner's (1992) encoding into the π-calculus. Exact operational and denotational characterizations for this equivalence are given. Second, Abramsky's applicative bisimulation is examined when the lambda calculus is augmented with (well-formed) operators, i.e. symbols equipped with reduction rules describing their behavior. Then, maximal discrimination is obtained when all operators are considered; it is shown that this discrimination coincides with the one given by the above equivalence and that the adoption of certain nondeterministic operators is sufficient and necessary to induce it

BibTeX

  @InProceedings{Sangiorgi-Thelazylambdacalcul,
    author = 	 {Sangiorgi, D.},
    title = 	 {The lazy lambda calculus in a concurrency scenario},
    booktitle =  {Proceedings of the Seventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1992},
    year =	 1992,
    editor =	 {Andre Scedrov},
    month =	 {June}, 
    pages =      {102--109},
    location =   {Santa Cruz, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }