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.

• Type: Conference
• Year: 2005
• Where: TLCA
• Authors: Nick Benton, Benjamin Leperchey
• Keywords: Equivalences Involving Allocation, Monadic Semantics, Relational Reasoning Principle, Theoretical Computer Science, TLCA 2005