Sciweavers

TLCA
2005
Springer

Relational Reasoning in a Nominal Semantics for Storage

13 years 9 months ago
Relational Reasoning in a Nominal Semantics for Storage
We give a monadic semantics in the category of FM-cpos to a higher-order CBV language with recursion and dynamically allocated mutable references that may store both ground data and the addresses of other references, but not functions. This model is adequate, though fully abstract. We then develop a relational reasoning principle over the denotational model, and show how it may be used to establish various contextual equivalences involving allocation and encapsulation of store.
Nick Benton, Benjamin Leperchey
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where TLCA
Authors Nick Benton, Benjamin Leperchey
Comments (0)