Title: Gradual Ownership Types
Authors: Sergey, Ilya
Clarke, Dave
Issue Date: Mar-2012
Publisher: Springer
Host Document: Programming Languages and Systems, ESOP 2012 vol:7211 pages:579-599
Series Title: Lecture Notes in Computer Science
Conference: European Symposium on Programming edition:21 location:Tallinn, Estonia date:24 March - 1 April 2012
Abstract: Gradual Ownership Types are a framework allowing programs to be partially annotated with ownership types, while providing the same encapsulation guarantees. The formalism provides a static guarantee of the desired encapsulation property for fully annotated programs, and dynamic guarantees for partially annotated programs via dynamic checks inserted by the compiler. This enables a smooth migration from ownership-unaware to ownership-typed code.
The paper provides a formal account of gradual ownership types. The theoretical novelty of this work is in adapting the notion of gradual type system with respect to program heap properties, which, unlike types in functional languages or object calculi, impose restrictions not only on data, but also on the environment the data is being processed in. From the practical side, we evaluate applicability of Gradual Ownership Types for Java 1.4 in the context of the Java Collection Framework and measure the necessary amount of annotations for ensuring the owners-as-dominators invariant.
ISBN: 978-3-642-28868-5
ISSN: 0302-9743
Publication status: published
KU Leuven publication type: IC
Appears in Collections:Informatics Section

Files in This Item:
File Description Status SizeFormat
ESOP.pdfMain article Accepted 288KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.

© Web of science