Lightweight Java

Lightweight Java (LJ) is an imperative fragment of Java [5]. 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. The accom-panying Isabelle script proves the type soundness of the Ott-generated LJ definition.