Militão, F, Aldrich J, Caires L.  2010.  Aliasing control with view-based typestate. Formal Techniques for Java Programs (FTfJP).