Lightweight Java (LJ) is a fully-formalized and extensible minimal imperative fragment of Java.
LJ is an imperative fragment of Java. It is intended to be as simple as possible while still retaining the feel of Java. LJ includes fields, methods, single inheritance, dynamic method dispatch, and method overriding. It does not include support for local variables, field hiding, interfaces, inner classes, or generics.
It is largely a simplification of Middleweight Java (MJ). A major difference w.r.t. Featherweight Java (FJ) is that LJ also models state, whereas FJ is purely functional. In this sense, LJ is similar to ClassicJava; however, unlike ClassicJava, LJ is a proper subset of Java, i.e. every LJ program is a valid Java program.
The Lightweight Java distributable [lj.zip] contains:
A detailed description of Lightweight Java's design and an overview of its type soundness proof can be found in the third chapter of my Ph.D. thesis.
The above documents and software are released under a BSD License.
There is also a Lightweight Java page on Wikipedia.