Title: Gradual ownership types
Authors: Sergey, Ilya
Clarke, Dave
Issue Date: Dec-2011
Publisher: Department of Computer Science, K.U.Leuven
Series Title: CW Reports vol:CW613
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. This leads, in particular, to runtime checks of a heap invariant, involving collections of objects.

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 annotations for ensuring the invariant. We also report on the performance drawbacks and a detected possible "ownership leak".
Publication status: published
KU Leuven publication type: IR
Appears in Collections:Informatics Section

Files in This Item:
File Description Status SizeFormat
CW613.pdfDocument Published 442KbAdobe PDFView/Open


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