JavaScript is disabled for your browser. Some features of this site may not work without it.
Relational Semantics of Local Variable Scoping

Author
Aboul-Hosn, Kamal; Kozen, Dexter
Abstract
Most previous work on the equivalence of programs in the presence of
local state has involved intricate memory modeling and the notion of contextual (observable) equivalence. We show how relational semantics can be used to avoid these complications. We define a notion of local variable scoping, along with a purely compositional semantics based on binary relations, such that all contextual considerations are completely encapsulated in the semantics. We then give an axiom system for program equivalence in the presence of local state that avoids all mention of memory or context and that does not use semantic arguments. The system is complete relative to the underlying flat equational theory. We also indicate briefly how the semantics can be extended to include higher-order functions.
Date Issued
2005-07-18Publisher
Cornell University
Subject
computer science; technical report
Previously Published As
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2005-2000
Type
technical report