Flexible recovery of uniqueness and immutability (Extended Version)

TL;DR

This paper introduces an expressive imperative object calculus with a novel type system that recovers uniqueness and immutability properties through a recovery approach, and models execution with a source-term-based operational semantics.

Contribution

It proposes a new type system that allows recovering aliasing and mutation properties, and a non-standard operational model based on source terms rather than auxiliary memory structures.

Findings

Type system effectively recovers uniqueness and immutability.

Operational semantics directly express qualifier properties on source terms.

Enhanced expressiveness compared to similar proposals.

Abstract

We present an imperative object calculus where types are annotated with qualifiers for aliasing and mutation control. There are two key novelties with respect to similar proposals. First, the type system is very expressive. Notably, it adopts the "recovery" approach, that is, using the type context to justify strengthening types, greatly improving its power by permitting to recover uniqueness and immutability properties even in presence of other references. This is achieved by rules which restrict the use of such other references in the portion of code which is recovered. Second, execution is modeled by a non standard operational model, where properties of qualifiers 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, when evaluated, play the role of store.