000135708 001__ 135708
000135708 005__ 20190316234529.0
000135708 037__ $$aREP_WORK
000135708 245__ $$aCapabilities for External Uniqueness
000135708 269__ $$a2009
000135708 260__ $$c2009
000135708 336__ $$aReports
000135708 520__ $$aUnique object references have many important applications in object-oriented programming. For instance, with sufficient encapsulation properties they enable safe and efficient transfer of message objects between concurrent processes. However, it is a long-standing challenge to integrate unique references into practical object-oriented programming languages. This paper introduces a new approach to external uniqueness. The idea is to use capabilities for enforcing both aliasing constraints that guarantee external uniqueness, and linear consumption of unique references. We formalize our approach as a type system, and prove a type preservation theorem. Type safety rests on an alias invariant that builds on a novel formalization of external uniqueness. We show how a capability-based type system can be used to integrate external uniqueness into widely available object- oriented programming languages. Practical experience suggests that our system allows adding uniqueness information to common collection classes in a simple and concise way.
000135708 6531_ $$aAliasing
000135708 6531_ $$aLinear types
000135708 6531_ $$aUnique pointers
000135708 6531_ $$aCapabilities
000135708 700__ $$0240993$$aHaller, Philipp$$g172057
000135708 700__ $$0241835$$aOdersky, Martin$$g126003
000135708 8564_ $$uhttp://lamp.epfl.ch/~phaller/uniquerefs/$$zURL
000135708 8564_ $$s407924$$uhttps://infoscience.epfl.ch/record/135708/files/capabilities_for_uniqueness_TR.pdf$$zn/a
000135708 909C0 $$0252187$$pLAMP$$xU10409
000135708 909CO $$ooai:infoscience.tind.io:135708$$pIC$$preport$$qGLOBAL_SET
000135708 937__ $$aLAMP-REPORT-2009-001
000135708 973__ $$aEPFL$$sPUBLISHED
000135708 980__ $$aREPORT