We suggest a model for dynamic loading and linking as in Java. We distinguish five components in a Java implementation: evaluation,
resolution, loading, verification, and preparation — with their associated checks. We demonstrate how these five together
guarantee type soundness.
We take an abstract view, and base our model on a language nearer to Java source than to bytecode. We consider the following
features of Java: classes, subclasses, fields and hiding, methods and inheritance, and interfaces.
This work was partly supported by EPSRC, Grant ref: GR/L 76709