OWNERSHIP TYPES FOR FLEXIBLE ALIAS PROTECTION

Object-oriented programming languages allow inter-object aliasing. Alt hough necessary to construct linked data structures and networks of in teracting objects, aliasing is problematic in that an aggregate object 's state can change via an alias to one of ifs components, without the aggregate being aware of any aliasing. Ownership types form a static type system that indicates object ownership. This provides a flexible mechanism to limit the visibility of object references and restrict ac cess paths to objects, thus controlling a system's dynamic topology. T he type system is shown to be sound, and the specific aliasing propert ies that a system's object graph satisfies are formulated and proven i nvariant for well-typed programs.