@comment{{This file has been generated by bib2bib 1.96}}
@comment{{Command line: /usr/bin/bib2bib -c topic:"java_modules" -ob topic.java_modules.bib sewellbib2.bib}}
  author = {Rok {Strni\v sa} and Peter Sewell and Matthew Parkinson},
  title = {The {J}ava {M}odule {S}ystem: core design and semantic definition},
  optcrossref = {},
  optkey = {},
  conf = {OOPSLA 2007},
  booktitle = {Proceedings of the {22nd ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages and Applications (Montre{\'a}l)}},
  optpages = {15 pp},
  pages = {499--514},
  numpages = {16},
  opturl = {},
  doi = {10.1145/1297027.1297064},
  year = {2007},
  opteditor = {},
  optvolume = {},
  optnumber = {},
  optseries = {},
  optaddress = {},
  month = oct,
  optorganization = {},
  optpublisher = {},
  optannote = {},
  project = {},
  pdf = {},
  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.},
  topic = {java_modules}