Global State Considered Helpful

13 years 6 months ago
Global State Considered Helpful
Reynolds' view of a storage cell as an expression-acceptor pair has been widely used by researchers. We present a different way of organizing semantics of state, and in particular game semantics, by adding to typing contexts a zone for global state. This has the following advantages. Firstly, it causes the "good variable" equations for references to be validated, and also the noninterference equations between distinct references, as enumerated by Plotkin and Power. Secondly, it gives a cleaner categorical structure based on the configurations (state + program) used to describe operational semantics. Thirdly, it leads to a simpler proof that the game semantics is sound and adequate with respect to the operational semantics.
Paul Blain Levy
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Authors Paul Blain Levy
Comments (0)