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

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 Fown, 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 firstclass functions, abstract data types, and parametric polymorphism. By looking at ownership in the setting of System F, we were able to develop a design that is more principled and flexible than previous ownership type systems, while also providing stronger encapsulation guarantees. Categories and Subject Descriptors D.3 [Programming Languages]: Language Constructs and Features General Terms Languages, T...

• Type: Conference
• Year: 2005
• Where: PLDI
• Authors: Neelakantan R. Krishnaswami, Jonathan Aldrich
• Keywords: Ownership Types, PLDI 2005, Programming Languages, System F, Type Theory