Article

Permission-based ownership: encapsulating state in higher-order typed languages

Authors:

Neel Krishnaswami,

Jonathan AldrichAuthors Info & Claims

PLDI '05: Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation

Pages 96 - 106

https://doi.org/10.1145/1065010.1065023

Published: 12 June 2005 Publication History

Abstract

Today's module systems do not effectively support information hiding in the presence of shared mutable objects, causing serious problems in the development and evolution of large software systems. Ownership types have been proposed as a solution to this problem, but current systems have ad-hoc access restrictions and are limited to Java-like languages.In this paper, we describe System F_own, an extension of System F with references and ownership. Our design shows both how ownership fits into standard type theory and the encapsulation benefits it can provide in languages with first-class functions, abstract data types, and parametric polymorphism. By looking at ownership in the setting of SystemF, we were able to develop a design that is more principled and flexible than previous ownership type systems, while also providing stronger encapsulation guarantees.

References

[1]

J. Aldrich and C. Chambers. Ownership Domains: Separating Aliasing Policy from Mechanism. In European Conference on Object-Oriented Programming, June 2004.]]

[2]

J. Aldrich, V. Kostadinov, and C. Chambers. Alias Annotations for Program Understanding. In Object-Oriented Programming Systems, Languages, and Applications, November 2002.]]

Digital Library

[3]

P. S. Almeida. Balloon Types: Controlling Sharing of State in Data Types. In European Conference on Object-Oriented Programming, June 1997.]]

[4]

A. Banerjee and D. A. Naumann. Representation Independence, Confinement, and Access Control. In Principles of Programming Languages, January 2002.]]

Digital Library

[5]

B. Bokowski and J. Vitek. Confined Types. In Object-Oriented Programming Systems, Languages, and Applications, November 1999.]]

Digital Library

[6]

C. Boyapati, R. Lee, and M. Rinard. Ownership Types for Safe Programming: Preventing Data Races and Deadlocks. In Object-Oriented Programming Systems, Languages, and Applications, November 2002.]]

Digital Library

[7]

C. Boyapati, A. Salcianu, J. William Beebee, and M. Rinard. Ownership Types for Safe Region-Based Memory Mangement in Real-Time Java. In Programming Language Design and Implementation, June 2003.]]

Digital Library

[8]

D. Clarke. Object Ownership & Containment. PhD thesis, University of New South Wales, July 2001.]]

Digital Library

[9]

D. Clarke and S. Drossopoulou. Ownership, Encapsulation, and the Disjointness of Type and Effect. In Object-Oriented Programming Systems, Languages, and Applications, November 2002.]]

Digital Library

[10]

D. G. Clarke, J. M. Potter, and J. Noble. Ownership Types for Flexible Alias Protection. In Object-Oriented Programming Systems, Languages, and Applications, October 1998.]]

Digital Library

[11]

D. G. Clarke, J. M. Potter, and J. Noble. Simple Ownership Types for Object Containment. In European Conference on Object-Oriented Programming, 2001.]]

Digital Library

[12]

M. Fahndrich and R. DeLine. Adoption and focus: Practical linear types for imperative programming. In Programming Language Design and Implementation, pages 13--24. ACM Press, 2002.]]

Digital Library

[13]

M. Fluet and G. Morisett. Monadic regions. In International Conference on Functional Programming, 2004.]]

Digital Library

[14]

C. Fournet and A. D. Gordon. Stack inspection: theory and variants. In Symposium on Principles of Programming Languages, pages 307--318, 2002.]]

Digital Library

[15]

A. Greenhouse and J. Boyland. An Object-Oriented Effects System. In European Conference on Object-Oriented Programming, June 1999.]]

Digital Library

[16]

D. Grossman, G. Morrisett, and S. Zdancewic. Syntactic Type Abstraction. Transactions on Programming Languages and Systems, 22(6):1037--1080, November 2000.]]

Digital Library

[17]

J. Hogg. Islands: Aliasing Protection in Object-Oriented Languages. In Object-Oriented Programming Systems, Languages, and Applications, October 1991.]]

Digital Library

[18]

Y. L. J-Y Girard and P. Taylor. Proofs and Types. Cambridge University Press, 1989.]]

Digital Library

[19]

K. R. M. Leino, A. Poetzsch-Heffter, and Y. Zhou. Using Data Groups to Specify and Check Side Effects. In Programming Language Design and Implementation, June 2002.]]

Digital Library

[20]

J. C. Mitchell and G. D. Plotkin. Abstract types have existential type. Transactions on Programming Languages and Systems, 10(3):470--502, 1988.]]

Digital Library

[21]

K. Miyamoto and A. Igarashi. A modal foundation for secure information flow. In Workshop on Foundations of Computer Security, pages 187--203, 2004.]]

[22]

J. Noble, J. Vitek, and J. Potter. Flexible Alias Protection. In European Conference on Object-Oriented Programming, 1998.]]

Digital Library

[23]

M. Odersky. Programming in Scala. Book draft available at http://scala.epfl.ch/, 2004.]]

[24]

P. W. O'Hearn, H. Yang, and J. C. Reynolds. Separation and information hiding. In Principles of Programming Languages, 2004.]]

Digital Library

[25]

D. L. Parnas. On the Criteria to be Used in Decomposing Systems into Modules. Communications of the ACM, 15(12):1053--1058, December 1972.]]

Digital Library

[26]

J. C. Reynolds. Separation Logic: a Logic for Shared Mutable Data Structures. In Logic in Computer Science, July 2002.]]

Digital Library

[27]

J.-P. Talpin and P. Jouvelot. The type and effect discipline. In Information and Computation, pages 245--296, 1994.]]

Digital Library

[28]

M. Tofte and J.-P. Talpin. Region-based memory management. Information and Computation, 132(2):109--176, 1997.]]

Digital Library

[29]

D. Walker and G. Morrisett. Alias Types for Recursive Data Structures. In International Workshop on Types in Compilation, September 2000.]]

Digital Library

Cited By

Crichton WGray GKrishnamurthi S(2023)A Grounded Conceptual Model for Ownership Types in RustProceedings of the ACM on Programming Languages10.1145/36228417:OOPSLA2(1224-1252)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622841
Fernandez-Reyes KGariano INoble JGreenwood-Thessman EHomer MWrigstad TDe Meuter WBaniassad E(2021)Dala: a simple capability-based dynamic language design for data race-freedomProceedings of the 2021 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software10.1145/3486607.3486747(1-17)Online publication date: 20-Oct-2021
https://dl.acm.org/doi/10.1145/3486607.3486747
Mycroft AVoigt J(2013)Notions of aliasing and ownershipAliasing in Object-Oriented Programming10.5555/2554511.2554517(59-83)Online publication date: 1-Jan-2013
https://dl.acm.org/doi/10.5555/2554511.2554517
Show More Cited By

Index Terms

Permission-based ownership: encapsulating state in higher-order typed languages
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages

Recommendations

Permission-based ownership: encapsulating state in higher-order typed languages
Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation

Today's module systems do not effectively support information hiding in the presence of shared mutable objects, causing serious problems in the development and evolution of large software systems. Ownership types have been proposed as a solution to this ...
On the power of coercion abstraction
POPL '12

Erasable coercions in System F-eta, also known as retyping functions, are well-typed eta-expansions of the identity. They may change the type of terms without changing their behavior and can thus be erased before reduction. Coercions in F-eta can model ...
On the power of coercion abstraction
POPL '12: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Erasable coercions in System F-eta, also known as retyping functions, are well-typed eta-expansions of the identity. They may change the type of terms without changing their behavior and can thus be erased before reduction. Coercions in F-eta can model ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI '05: Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation

June 2005

338 pages

ISBN:1595930566

DOI:10.1145/1065010

General Chair:
Vivek Sarkar
IBM Research
,
Program Chair:
Mary Hall
USC/ISI

ACM SIGPLAN Notices Volume 40, Issue 6
Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation
June 2005
325 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1064978
Issue’s Table of Contents

Copyright © 2005 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 June 2005

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

PLDI05

Sponsor:

PLDI05: ACM SIGPLAN Conference on Programming Language Design and Implementation 2005

June 12 - 15, 2005

IL, Chicago, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

25
Total Citations
View Citations
476
Total Downloads

Downloads (Last 12 months)6
Downloads (Last 6 weeks)1

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Crichton WGray GKrishnamurthi S(2023)A Grounded Conceptual Model for Ownership Types in RustProceedings of the ACM on Programming Languages10.1145/36228417:OOPSLA2(1224-1252)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622841
Fernandez-Reyes KGariano INoble JGreenwood-Thessman EHomer MWrigstad TDe Meuter WBaniassad E(2021)Dala: a simple capability-based dynamic language design for data race-freedomProceedings of the 2021 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software10.1145/3486607.3486747(1-17)Online publication date: 20-Oct-2021
https://dl.acm.org/doi/10.1145/3486607.3486747
Mycroft AVoigt J(2013)Notions of aliasing and ownershipAliasing in Object-Oriented Programming10.5555/2554511.2554517(59-83)Online publication date: 1-Jan-2013
https://dl.acm.org/doi/10.5555/2554511.2554517
Clarke DÖstlund JSergey IWrigstad T(2013)Ownership typesAliasing in Object-Oriented Programming10.5555/2554511.2554516(15-58)Online publication date: 1-Jan-2013
https://dl.acm.org/doi/10.5555/2554511.2554516
Mycroft AVoigt J(2013)Notions of Aliasing and OwnershipAliasing in Object-Oriented Programming. Types, Analysis and Verification10.1007/978-3-642-36946-9_4(59-83)Online publication date: 2013
https://doi.org/10.1007/978-3-642-36946-9_4
Dietl WDrossopoulou SMüller P(2012)Separating ownership topology and encapsulation with generic universe typesACM Transactions on Programming Languages and Systems10.1145/2049706.204970933:6(1-62)Online publication date: 3-Jan-2012
https://dl.acm.org/doi/10.1145/2049706.2049709
Patrignani MClarke DSangiorgi D(2011)Ownership types for the join calculusProceedings of the joint 13th IFIP WG 6.1 and 30th IFIP WG 6.1 international conference on Formal techniques for distributed systems10.5555/2022067.2022086(289-303)Online publication date: 6-Jun-2011
https://dl.acm.org/doi/10.5555/2022067.2022086
Patrignani MClarke DSangiorgi D(2011)Ownership Types for the Join CalculusFormal Techniques for Distributed Systems10.1007/978-3-642-21461-5_19(289-303)Online publication date: 2011
https://doi.org/10.1007/978-3-642-21461-5_19
Cameron NDietl W(2009)Comparing universes and existential ownership typesInternational Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming10.1145/1562154.1562163(1-8)Online publication date: 6-Jul-2009
https://dl.acm.org/doi/10.1145/1562154.1562163
Cameron NNoble J(2009)OGJ gone wildInternational Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming10.1145/1562154.1562161(1-10)Online publication date: 6-Jul-2009
https://dl.acm.org/doi/10.1145/1562154.1562161
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten