Inference and Checking of Object Ownership

Date Added: May 2012
Format: PDF

Ownership type systems describe a heap topology and enforce an encapsulation discipline; they aid in various program correctness and understanding tasks. However, the annotation overhead of ownership type systems has hindered their widespread use. The authors present a unified framework for specification, type inference and type checking of ownership type systems, and instantiate the framework for two such systems: Universe Types and Ownership Types. They present an objective metric defining a "Best typing" for these type systems, and develop an inference approach that maximizes the metric. The programmer can influence the inference by adding partial annotations to the program.