@inproceedings{strnia2007the,
author = {Strniša, Rok and Sewell, Peter and Parkinson, Matthew J.},
title = {The java module system: core design and semantic definition},
series = {OOPSLA '07},
booktitle = {Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems and applications},
year = {2007},
month = {January},
abstract = {Java has no module system. Its packages only subdivide the class name space, allowing only a very limited form of component-level information hiding and reuse. Two Java Community Processes have started addressing this problem: one describes the runtime system and has reached an early draft stage, while the other considers the developer's view and only has a straw-man proposal. Both are natural language documents, which inevitably contain ambiguities.

In this work we design and formalize a core module system for Java. Where the JCP documents are complete, we follow them closely; elsewhere we make reasonable choices. We define the syntax, the type system, and the operational semantics of an LJAM language, defining these rigorously in the Isabelle/HOL automated proof assistant. Using this formalization, we identify various issues with the module system. We highlight the underlying design decisions, and discuss several alternatives and their benefits. Our Isabelle/HOL definitions should provide a basis for further consideration of the design alternatives, for reference implementations, and for proofs of soundness.},
publisher = {ACM},
url = {http://approjects.co.za/?big=en-us/research/publication/the-java-module-system-core-design-and-semantic-definition/},
pages = {499-514},
isbn = {978-1-59593-786-5},
edition = {Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems and applications},
}