Tracking Linear and Affine Resources with Java(X)

Markus Degen, Peter Thiemann, and Stefan Wehr

In Erik Ernst, editor, Proceedings of the European Conference on Object-Oriented Programming. Lecture Notes in Computer Science, vol. 4609, pp. 550-574, Berlin, Germany. Springer, 2007.

Abstract

Java(X) is a framework for type refinement. It extends Java's type language with annotations drawn from an algebra X and structural subtyping in terms of the annotations. Each instantiation of X yields a different refinement type system with guaranteed soundness. The paper presents some applications, formalizes a core language, states a generic type soundness result, and sketches the extensions required for the full Java language (without generics).

The main technical innovation of Java(X) is its concept of activity annotations paired with the notion of droppability. An activity annotation is a capability which can grant exclusive write permission for a field in an object and thus facilitates a typestate change (strong update). Propagation of capabilities is either linear or affine (if they are droppable). Thus, Java(X) can perform protocol checking as well as refinement typing. Aliasing is addressed with a novel splitting relation on types.

Bibtex

@INPROCEEDINGS{DegenThiemannWehr2007,
  author = {Markus Degen and Peter Thiemann and Stefan Wehr},
  title = {Tracking Linear and Affine Resources with {Java(X)}},
  address = {Berlin, Germany},
  year = 2007,
  booktitle = {Proceedings of the European Conference on Object-Oriented Programming},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  volume = 4609,
  pages = {550--574},
  editor = {Erik Ernst}
}

Resources

• Preprint: .pdf (© Springer-Verlag)
• Type checker: .tar.gz
• Publisher's version: http://dx.doi.org/10.1007/978-3-540-73589-2_26
• Acceptance rate: 18.5 % (135 papers reviewed, 25 accepted)