- Rok Strniša
- improved Java Module System
improved Java Module System
improved Java Module System (iJAM) is an extension of Lightweight Java Module
System that gives a more expressive &
iJAM solves the following two deficiencies with the proposed Java Module System (and formalised within LJAM) that we have identified:
- Unintuitive lookup functions for module and class definitions.
- Too restricted initialization of module definitions.
The language 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.
- Fixing the Java Module System, in Theory and in Practice
- Definition in Ott 0.20.1
[lj_common.ott, ljam_commoni.ott, ljp_basei.ott, ljm_basei.ott, ljami.ott] (+ README.txt, Makefile, iJAM.tex).
- Grammar, Typing, and Small-Step Operational
Semantics (generated by Ott, re-ordered).
- Definition in Isabelle/HOL 2008 (generated
- Implementation of iJAM
- Proof of iJAM'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