A Fully Abstract Semantics for Concurrent Graph Reduction

abstract semantics for concurrent graph reduction ALAN JEFFREY This paper presents a fully abstract semantics for a variant of the untyped -calculus with recursive declarations. We first present a summary of existing work on full abstraction for the untyped -calculus, concentrating on ABRAMSKY and ONG's work on the lazy -calculus. ABRAMSKY and ONG'swork is based on leftmost outermost reduction without sharing. This is notably inefficient, and many implementations model sharing by reducing syntax graphs rather than syntax trees. Here we present a concurrent graph reduction algorithm for the -calculus with recursive declarations, in a milar to BERRY and BOUDOL'sChemical 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. Contents

• Type: Conference
• Year: 1994
• Where: LICS
• Authors: Alan Jeffrey
• Keywords: Abstract Semantics, Automated Reasoning, Concurrent Graph Reduction, LICS 1994, Recursive Declarations