- Lightweight Java Module System
Lightweight Java Module System
Lightweight Java Module System (LJAM) is the core design and semantic definition of a Java Module
LJAM is Lightweight Java (LJ) extended with a module
system based on early drafts for the Java Module System: it covers the core
parts of both JSR-277 and
JSR-294. For those
aspects in the scope of the former, we
informal description closely; for the remainder, we try to capture what
we believe is the intended semantics. At the time of development of LJAM,
JSR-294 only a simple straw-man proposal (which is no longer
The language was designed and formalized by Rok Strniša.
LJAM 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 Java Module System: Core Design and Semantic Definition (OOPSLA'07
paper, © ACM, 2007) [pdf]
- Definition in Ott 0.20.1
[lj_common.ott, ljam_common.ott, ljp_base.ott, ljm_base.ott, ljam.ott]
(+ README.txt, Makefile, ljam.tex).
- Grammar, Typing, and Small-Step Operational
Semantics (generated by Ott, re-ordered).
- Definition in Isabelle/HOL 2008 (generated
- Proof of LJAM's progress and well-formedness
preservation in Isabelle/HOL 2008
- A graph of dependencies between lemmas and
The above software is released under a New BSD