File(s) stored somewhere else

Please note: Linked content is NOT stored on Open Access Victoria University of Wellington | Te Herenga Waka and we can't guarantee its availability, quality, security or accept any liability.

Flexible recovery of uniqueness and immutability

journal contribution
posted on 01.11.2020, 22:39 by P Giannini, Marco Servetto, E Zucca, J Cone
© 2018 Elsevier B.V. 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.

History

Preferred citation

Giannini, P., Servetto, M., Zucca, E. & Cone, J. (2019). Flexible recovery of uniqueness and immutability. Theoretical Computer Science, 764, 145-172. https://doi.org/10.1016/j.tcs.2018.09.001

Journal title

Theoretical Computer Science

Volume

764

Publication date

11/04/2019

Pagination

145-172

Publisher

Elsevier BV

Publication status

Published

ISSN

0304-3975

eISSN

1879-2294

Language

en

Exports