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.
Scheda prodotto non validato
Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo
|Titolo:||Aliasing control in an imperative pure calculus|
|Data di pubblicazione:||2015|
|Appare nelle tipologie:||04.01 - Contributo in atti di convegno|