Abstract
In this paper we will explore the relationship between Ownership Types and more fundamental type systems. In particular, we show that ownership types (in both simple and embellished flavours) are dependent types by translating object calculi with object ownership to lambda calculi with dependent types. We discuss which ownership features share features in the underlying dependent type system, and which additional features require additional complexity.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Clarke, D.G., Potter, J.M., Noble, J.: Ownership Types for Flexible Alias Protection. In: Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA (1998)
Clarke, D.G.: Object Ownership and Containment. PhD thesis, School of Computer Science and Engineering, The University of New South Wales, Sydney, Australia (2001)
Aspinall, D., Hofmann, M.: Dependent types. In: Pierce, B.C. (ed.) Advanced Topics in Types and Programming Languages, The MIT Press (2004)
Potanin, A., Noble, J., Clarke, D., Biddle, R.: Generic Ownership for Generic Java. In: Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA (2006)
Cameron, N., Noble, J.: Encoding Ownership Types in Java. In: Vitek, J. (ed.) TOOLS 2010. LNCS, vol. 6141, pp. 271–290. Springer, Heidelberg (2010)
McKinna, J.: Why dependent types matter. In: Symposium on Principles of Programming Languages, POPL (2006)
Xi, H., Pfenning, F.: Dependent types in practical programming. In: Symposium on Principles of Programming Languages, POPL (1999)
McBride, C., McKinna, J.: The view from the left. Journal of Functional Programming 14(1), 69–111 (2004)
Clarke, D.G., Drossopoulou, S.: Ownership, Encapsulation and the Disjointness of Type and Effect. In: Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA (2002)
Bruce, K.B., Cardelli, L., Pierce, B.C.: Comparing Object Encodings. Information and Computation 155(1-2) (1999)
Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: a Minimal Core Calculus For Java and GJ. Transactions on Programming Languages and Systems 23(3), 396–450 (2001); An earlier version of this work appeared at OOPSLA 1999
Cameron, N., Drossopoulou, S., Noble, J.: Understanding Ownership Types with Dependent Types. Technical report 23, Vistoria University, School of Engineering and Computer Science (2012)
Dietl, W., Drossopoulou, S., Müller, P.: Generic Universe Types. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 28–53. Springer, Heidelberg (2007)
Lu, Y.: On Ownership and Accessibility. In: Thomas, D. (ed.) ECOOP 2006. LNCS, vol. 4067, pp. 99–123. Springer, Heidelberg (2006)
Mitchell, J.C., Plotkin, G.D.: Abstract Types have Existential Type. Transactions on Programming Languages and Systems 10(3), 470–502 (1988)
Wadler, P.: Comprehending monads. In: Conference on LISP and Functional Programming, LFP (1990)
Wrigstad, T.: Ownership-Based Alias Managemant. PhD thesis, KTH, Sweden (2006)
Dietl, W., Drossopoulou, S., Müller, P.: Separating ownership topology and encapsulation with Generic Universe Types. Transactions on Programming Languages and Systems (TOPLAS) 33 20, 20:1–20:62 (2011)
Cameron, N., Drossopoulou, S., Noble, J., Smith, M.: Multiple Ownership. In: Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA (2007)
Zhao, T., Palsberg, J., Vitek, J.: Type-based Confinement. J. Funct. Program 16(1), 83–128 (2006)
Cameron, N., Drossopoulou, S.: Existential Quantification for Variant Ownership. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 128–142. Springer, Heidelberg (2009)
Müller, P.: Modular Specification and Verification of Object-Oriented Programs. LNCS, vol. 2262. Springer, Heidelberg (2002)
Lu, Y., Potter, J.: Protecting Representation with Effect Encapsulation. In: Principles of Programming Languages, POPL (2006)
Wrigstad, T., Clarke, D.G.: Existential Owners for Ownership Types. Journal of Object Technology 6(4) (2007)
Cameron, N., Dietl, W.: Comparing Universes and Existential Ownership Types. In: International Workshop on Aliasing, Confinement and Ownership in object-oriented programming, IWACO (2009)
Cameron, N.: Existential Types for Variance — Java Wildcards and Ownership Types. PhD thesis, Imperial College London (2009)
Aldrich, J., Chambers, C.: Ownership Domains: Separating Aliasing Policy from Mechanism. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 1–25. Springer, Heidelberg (2004)
Hinze, R.: Fun with phantom types. In: The Fun of Programming, pp. 245–262. Palgrave Macmillan (2003)
Cameron, N., Noble, J.: OGJ Gone Wild. In: International Workshop on Aliasing, Confinement and Ownership in object-oriented programming, IWACO (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Cameron, N., Drossopoulou, S., Noble, J. (2013). Understanding Ownership Types with Dependent Types. In: Clarke, D., Noble, J., Wrigstad, T. (eds) Aliasing in Object-Oriented Programming. Types, Analysis and Verification. Lecture Notes in Computer Science, vol 7850. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-36946-9_5
Download citation
DOI: https://doi.org/10.1007/978-3-642-36946-9_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-36945-2
Online ISBN: 978-3-642-36946-9
eBook Packages: Computer ScienceComputer Science (R0)