Lightweight Java


Lightweight Java is a fully formalized and extensible minimal imperative fragment of Java. The language was designed for academic purposes within the Computer Laboratory, University of Cambridge. The definition of LJ was proven type-sound in Isabelle/HOL.