Abstract
This paper presents a fully abstract semantics for a variant of the untyped /spl lambda/-calculus with recursive [Bdeclarations. We first present a summary of existing work on full abstraction for the untyped /spl lambda/-calculus, concentrating on S. Abramsky (1989) and C.H.L. Ong (1988) work on the lazy /spl lambda/-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 /spl lambda/-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 /spl lambda/-calculus with recursive declarations, and show that the three semantics are equivalent.

This publication has 12 references indexed in Scilit: