Is the Java type system sound?

A proof of the soundness of the Java type system is a first, necessary step towards demonstrating which Java programs won't compromise computer securi ty. We consider a subset of Java describing primitive types, classes, inher itance, instance variables and methods, interfaces, shadowing, dynamic meth od binding, object creation, null, arrays, and exception throwing and handl ing. We argue that for this subset the type system is sound, by proving tha t program execution preserves the types, up to subclasses/subinterfaces. (C ) 1999 John Wiley & Sons, Inc.