Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell Computing and Information Science
  3. Computing and Information Science
  4. Computing and Information Science Technical Reports
  5. Relational Semantics of Local Variable Scoping

Relational Semantics of Local Variable Scoping

File(s)
TR2005-2000.pdf (171.05 KB)
Permanent Link(s)
https://hdl.handle.net/1813/5700
Collections
Computing and Information Science Technical Reports
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-18
Publisher
Cornell University
Keywords
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

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance