topic.java_modules.group.bib

@comment{{This file has been generated by bib2bib 1.99}}
@comment{{Command line: bibtex2html-1.99-with-magiclink/bib2bib -c topic:"java_modules" -ob topic.java_modules.group.bib groupbib.bib}}
@inproceedings{iJAM,
  author = {Rok Strni{\v s}a},
  title = {{Fixing the Java Module System, in Theory and in Practice}},
  conf = {FTfJP 2008},
  booktitle = {FTfJP '08: 10th Workshop on Formal Techniques for Java-like
                  Programs},
  location = {Paphos, Cyprus},
  month = jul # {~8,},
  year = 2008,
  note = {The informal proceedings are available as technical report ICIS-R08013 from the Radboud University, \url{https://www-sop.inria.fr/everest/events/FTfJP08/ftfjp08.pdf}},
  pdf = {http://www.cl.cam.ac.uk/~pes20/group_papers/ftfjp08-strnisa.pdf},
  abstract = {The proposed Java Module System (JAM) has two major deficiencies,
as noted in our previous work: (a) its unintuitive class resolution can often
give unexpected results; and (b) only a single instance of each module is permitted,
which forces sharing of data and types, and so makes it difficult to reason
about module invariants. Since JAM will be a part of Java 7, solving these problems
before its release would benefit the majority of Java developers and users.
In this paper, we propose modest changes to the module language, and to the
semantics of the class resolution, which together allow the module system to
handle more scenarios in a clean and predictable manner. To develop confidence,
both theoretical and practical, in our proposals, we: (a) formalise the improved
module system, iJAM; (b) prove mechanized type soundness results; and, (c) give
a proof-of-concept implementation that closely follows the formalisation; these
are in Ott, Isabelle/HOL, and Java, respectively.
The formalisation is itself modular: iJAM is based on our previous formalization
of JAM (LJAM), which extends Lightweight Java (LJ). LJ has shown to be
a good base language, allowing a high reuse of the definitions and proof scripts,
which made it possible to carry out this development relatively quickly, on the
timescale of the language evolution process.},
  project = {https://rok.strnisa.com/research/ijam/},
  topic = {java_modules}
}
@article{DBLP:journals/afp/StrnisaP11,
  author = {Rok Strnisa and
               Matthew J. Parkinson},
  title = {Lightweight Java},
  journal = {Archive of Formal Proofs},
  volume = {2011},
  year = {2011},
  html = {https://www.isa-afp.org/entries/LightweightJava.shtml},
  timestamp = {Mon, 19 Sep 2016 15:58:56 +0200},
  biburl = {http://dblp.uni-trier.de/rec/bib/journals/afp/StrnisaP11},
  bibsource = {dblp computer science bibliography, http://dblp.org},
  abstract = {A fully-formalized and extensible minimal imperative fragment of Java.},
  topic = {java_modules}
}
@phdthesis{RokStrnisaPhD,
  author = {Rok Strni{\v s}a},
  title = {Formalising, improving, and reusing the Java Module System},
  school = {University of Cambridge},
  year = {2010},
  optkey = {},
  opttype = {},
  optaddress = {},
  optmonth = {},
  optnote = {},
  optannote = {},
  pdf = {http://www.cl.cam.ac.uk/~pes20/group_papers/RokStrnisaPhD.pdf},
  abstract = {Java has no module system. Its packages only subdivide the class namespace, allowing
only a very limited form of component-level information hiding. A Java Community
Process has started designing the Java Module System, a module system for Java 7, the
next version of Java. The extensive draft of the design is written only in natural language
documents, which inevitably contain many ambiguities.

We design and formalise LJAM, a core of the module system. Where the informal
documents are complete, we follow them closely; elsewhere, we make reasonable choices.
We define the syntax, the type system, and the operational semantics of this core, defining
these rigorously in the Isabelle/HOL automated proof assistant. We highlight the underlying
design decisions, and discuss several alternatives and their benefits.

Through analysis of our formalisation, we identify two major deficiencies of the
module system: (a) its class resolution is unintuitive, insufficiently expressive, and fragile
against incremental interface evolution; and (b) only a single instance of each module
is permitted, which forces sharing of data and types, and so makes it difficult to reason
about module invariants. We propose modest changes to the module language, and to the
semantics of the class resolution, which together allow the module system to handle more
scenarios in a clean and predictable manner. To develop confidence, both theoretical and
practical, in our proposals, we (a) formalise in Ott the improved module system, iJAM, (b)
prove in Isabelle/HOL mechanised type soundness results, and (c) give a proof-of-concept
implementation in Java that closely follows the formalisation.

Both of the formalisations, LJAM and iJAM, are based on Lightweight Java (LJ),
our minimal imperative fragment of Java. LJ has been a good base language, allowing
a high reuse of the definitions and proof scripts, which made it possible to carry out this
development relatively quickly, on the timescale of the language evolution process.

Finally, we develop a module system for Thorn, an emerging, Java-like language
aimed at distributed environments. We find that local aliasing and module-prefixed type
references remove the need for boundary renaming, and that in the presence of multiple
module instances, care is required to avoid ambiguities at de-serialisation.

We conclude with a high-level overview of the interactions between the desired
properties and the language features considered, and discuss possible future directions.},
  topic = {java_modules}
}