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
