Encoding Ownership Types in Java

Nicholas Cameron and James Noble

Ownership type systems organise the heap into a hierarchy which can be used to support encapsulation properties, effects, and invariants. Ownership types have many applications including parallelisation, concurrency, memory management, and security. In this paper, we show that several flavours and extensions of ownership types can be entirely encoded using the standard Java type system.

Ownership types systems usually require a sizable effort to implement and the relation of ownership types to standard type systems is poorly understood. Our encoding demonstrates the connection between ownership types and parametric and existential types. We formalise our encoding using a model for Java's type system, and prove that it is sound and enforces an ownership hierarchy. Finally, we leverage our encoding to produce lightweight compilers for Ownership Types and Universe Types --- each compiler took only one day to implement.

Submitted for consideration to TOOLS Europe 2010

Download proofs

Download ownership types compiler
  • OTs.zip: Ownership Types pre-processor

Download Generic Universes Compiler
  • gut.zip: Generic Universes Types pre-processor