Lightweight Java

Lightweight Java (LJ) is a fully formalized and extensible minimal imperative fragment of Java.^[1]^[2] 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.^[3]

References

^ Strniša, Rok; Sewell, Peter; Parkinson, Matthew (2007年10月21日). "The java module system: Core design and semantic definition" . ACM SIGPLAN Notices. 42 (10). Association for Computing Machinery: 499–514. doi:10.1145/1297105.1297064. ISBN 978-1-59593-786-5.
^ Strniša, Rok. "Lightweight Java". rok.strnisa.com. Retrieved 2019年11月25日.
^ Strniša, Rok; Parkinson, Matthew (2011年02月07日). "Lightweight Java". Archive of Formal Proofs (Feb 2011 ed.). ISSN 2150-914X . Retrieved 2019年11月25日.