Lightweight Java

Lightweight Java (LJ) is a fully formalized and extensible minimal imperative fragment of Java.{{Cite journal |last1= Strniša |first1= Rok |last2= Sewell |first2 =Peter |last3 =Parkinson |first3 =Matthew |title= The java module system: Core design and semantic definition |journal= ACM SIGPLAN Notices |date= 2007-10-21 |url= http://portal.acm.org/citation.cfm?doid=1297105.1297064 |language= en |publisher= Association for Computing Machinery |volume= 42 |issue= 10 |pages= 499–514 |doi= 10.1145/1297105.1297064 |isbn= 978-1-59593-786-5 |url-access= subscription }}{{Cite web |url= https://rok.strnisa.com/research/lj/ |title= Lightweight Java |website= rok.strnisa.com |last= Strniša |first= Rok |access-date= 2019-11-25}} 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.{{Cite journal |last1= Strniša |first1= Rok |last2= Parkinson |first2= Matthew |date= 2011-02-07 |title= Lightweight Java |url= https://www.isa-afp.org/entries/LightweightJava.html |access-date= 2019-11-25 |journal= Archive of Formal Proofs |edition= Feb 2011 |issn= 2150-914X }}