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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M., Cardelli, L.: A Theory of Objects. Springer-Verlag New York, Inc., Secaucus (1996)
Aldrich, J., Chambers, C.: Ownership Domains: Separating Aliasing Policy from Mechanism. In: Vetta, A. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 1–25. Springer, Heidelberg (2004)
Boyapati, C., Liskov, B., Shrira, L.: Ownership types for object encapsulation. In: POPL 2003, pp. 213–223. ACM (2003)
Boyapati, C., Rinard, M.: A parameterized type system for race-free Java programs. In: OOPSLA 2001, pp. 56–69. ACM (2001)
Boyapati, C., Salcianu, A., Beebee Jr., W., Rinard, M.: Ownership types for safe region-based memory management in real-time Java. In: PLDI 2003, pp. 324–337. ACM (2003)
Cameron, N., Drossopoulou, S.: Existential Quantification for Variant Ownership. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 128–142. Springer, Heidelberg (2009)
Cameron, N.R., Drossopoulou, S., Noble, J., Smith, M.J.: Multiple ownership. In: OOPSLA 2007, pp. 441–460. ACM (2007)
Clarke, D., Drossopoulou, S.: Ownership, encapsulation and the disjointness of type and effect. In: OOPSLA 2002, pp. 292–310. ACM (2002)
Clarke, D., Wrigstad, T.: External Uniqueness is Unique Enough. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol. 2743, pp. 176–200. Springer, Heidelberg (2003)
Clarke, D.G.: Object ownership and containment. PhD thesis, University of New South Wales, New South Wales, Australia (2001)
Clarke, D.G., Potter, J.M., Noble, J.: Ownership types for flexible alias protection. In: OOPSLA 1998, pp. 48–64. ACM (1998)
Dietl, W., Ernst, M.D., Müller, P.: Tunable Static Inference for Generic Universe Types. In: Mezini, M. (ed.) ECOOP 2011. LNCS, vol. 6813, pp. 333–357. Springer, Heidelberg (2011)
Ekman, T., Hedin, G.: The JastAdd extensible Java compiler. In: OOPSLA 2007, pp. 1–18. ACM (2007)
Felleisen, M., Findler, R.B., Flatt, M.: Semantics Engineering with PLT Redex, 1st edn. The MIT Press (August 2009)
Flanagan, C.: Hybrid type checking. In: POPL 2006, pp. 245–256. ACM (2006)
Gordon, D., Noble, J.: Dynamic ownership in a dynamic language. In: DLS 2007, pp. 41–52. ACM (2007)
Ina, L., Igarashi, A.: Gradual typing for generics. In: OOPSLA 2011, pp. 609–624. ACM (2011)
Lu, Y., Potter, J.: On Ownership and Accessibility. In: Hu, Q. (ed.) ECOOP 2006. LNCS, vol. 4067, pp. 99–123. Springer, Heidelberg (2006)
Ma, K.-K., Foster, J.S.: Inferring aliasing and encapsulation properties for Java. In: OOPSLA 2007, pp. 321–336. ACM (2007)
Milanova, A., Vitek, J.: Static Dominance Inference. In: Bishop, J., Vallecillo, A. (eds.) TOOLS 2011. LNCS, vol. 6705, pp. 211–227. Springer, Heidelberg (2011)
Moelius III, S.E., Souter, A.L.: An object ownership inference algorithm and its applications. In: MASPLAS 2004 (2004)
Odersky, M., Cremet, V., Röckl, C., Zenger, M.: A Nominal Theory of Objects with Dependent Types. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol. 2743, pp. 201–224. Springer, Heidelberg (2003)
Pierce, B.C.: Types and programming languages. MIT Press, Cambridge (2002)
Potanin, A., Noble, J., Clarke, D., Biddle, R.: Generic ownership for generic Java. In: OOPSLA 2006, pp. 311–324. ACM (2006)
Sergey, I., Clarke, D.: Gradual Ownership Types. Technical Report Report CW 613, Katholieke Universiteit Leuven (December 2011)
Siek, J., Taha, W.: Gradual typing for functional languages. In: Scheme 2006 (2006)
Siek, J., Taha, W.: Gradual Typing for Objects. In: Bateni, M. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 2–27. Springer, Heidelberg (2007)
Vitek, J., Bokowski, B.: Confined types. In: OOPSLA 1999, pp. 82–96. ACM (1999)
Wadler, P., Findler, R.B.: Well-Typed Programs Can’t Be Blamed. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 1–16. Springer, Heidelberg (2009)
Wolff, R., Garcia, R., Tanter, É., Aldrich, J.: Gradual Typestate. In: Mezini, M. (ed.) ECOOP 2011. LNCS, vol. 6813, pp. 459–483. Springer, Heidelberg (2011)
Wren, A.: Inferring ownership. Master’s thesis, Imperial College London, UK (June 2003)
Wrigstad, T., Clarke, D.: Existential owners for ownership types. Journal of Object Technology 6(4) (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sergey, I., Clarke, D. (2012). Gradual Ownership Types. In: Seidl, H. (eds) Programming Languages and Systems. ESOP 2012. Lecture Notes in Computer Science, vol 7211. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28869-2_29
Download citation
DOI: https://doi.org/10.1007/978-3-642-28869-2_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28868-5
Online ISBN: 978-3-642-28869-2
eBook Packages: Computer ScienceComputer Science (R0)