Lightweight Java

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.

LJ is formalized rigorously: using the Ott tool, we obtain the typeset rules and its formal definition (in Isabelle/HOL) from the same source --- its Ott source files.

The language was designed and formalized by Rok Strniša and Matthew Parkinson.


The Lightweight Java distributable [] contains:

An up-to-date Isabelle/HOL proof of Lightweight Java's progress and well-formedness preservation can now be found at The Archive of Formal Proofs.

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.