Paper: A fully abstract semantics for concurrent graph reduction (at LICS 1994)

Authors: Alan Jeffrey

Abstract

This paper presents a fully abstract semantics for a variant of the untyped λ-calculus with recursive [Bdeclarations. We first present a summary of existing work on full abstraction for the untyped λ-calculus, concentrating on S. Abramsky (1989) and C.H.L. Ong (1988) work on the lazy λ-calculus. Abramsky and Ong's work is based on leftmost outermost reduction without sharing. This is notably inefficient, and many implementations model share by reducing syntax graphs rather than syntax trees. Here we present a concurrent graph reduction algorithm for the λ-calculus with recursive declarations, in a style similar to G. Berry and G. Boudol's chemical abstract machine. We adapt Abramsky and Ong's techniques, and present a program logic and denotational semantics for the λ-calculus with recursive declarations, and show that the three semantics are equivalent

BibTeX

  @InProceedings{Jeffrey-Afullyabstractseman,
    author = 	 {Alan Jeffrey},
    title = 	 {A fully abstract semantics for concurrent graph reduction},
    booktitle =  {Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS 1994)},
    year =	 {1994},
    month =	 {July}, 
    pages =      {82--91},
    location =   {Paris, France}, 
    publisher =	 {IEEE Computer Society Press}
  }