Aliasing control in an imperative pure calculus

We present an imperative object calculus where types are annotated with two modifiers for aliasing control. The lent modifier prevents objects to be aliased, whereas the capsule modifier characterizes expressions that will reduce to isolated portions of store. There are two key novelties w.r.t. similar proposals. First, the expressivity of the type system is greatly enhanced by promotion and swapping rules. The former recognizes as capsule an expression which only uses external references as lent. The latter allows a lent reference to be freely aliased, if all the other references are regarded as lent. Second, execution is modeled in a pure setting, where it is simpler to understand alias control. That is, properties of modifiers can be directly expressed on source terms, rather than as invariants on an auxiliary structure which mimics physical memory. Formally, this is achieved by the block construct, introducing local variable declarations, which play the role of store when evaluated