Sciweavers

ECOOP
2007
Springer

Tracking Linear and Affine Resources with Java(X)

13 years 7 months ago
Tracking Linear and Affine Resources with Java(X)
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.
Markus Degen, Peter Thiemann, Stefan Wehr
Added 14 Aug 2010
Updated 14 Aug 2010
Type Conference
Year 2007
Where ECOOP
Authors Markus Degen, Peter Thiemann, Stefan Wehr
Comments (0)