Sciweavers

Share
LICS
1994
IEEE

A Fully Abstract Semantics for Concurrent Graph Reduction

9 years 5 months ago
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
Alan Jeffrey
Added 09 Aug 2010
Updated 09 Aug 2010
Type Conference
Year 1994
Where LICS
Authors Alan Jeffrey
Comments (0)
books