An Imperative Pure Calculus

We present a simple calculus where imperative features are modeled by just rewriting source code terms, rather than by modifying an auxiliary structure which mimics physical memory. Formally, this is achieved by the block construct, introducing local variable declarations, which also plays the role of store when such declarations have been evaluated. In this way, we obtain a language semantics which is more abstract, and directly represents at the syntactic level constraints on aliasing, allowing simpler reasoning about related properties. We illustrate this possibility by a simple extension of the standard type system which assigns a capsule tag to expressions that will reduce to (values representing) isolated portions of store.