Flexible recovery of uniqueness and immutability

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...

Full description

Saved in:
Bibliographic Details
Published in:Theoretical computer science 2019-04, Vol.764, p.145-172
Main Authors: Giannini, Paola, Servetto, Marco, Zucca, Elena, Cone, James
Format: Article
Language:English
Subjects:
Aliasing
Immutability
Imperative calculi
Type systems
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0304-3975
1879-2294
DOI:10.1016/j.tcs.2018.09.001