Computing Publications

Publications Home » Is the Java Type System is Sound

Is the Java Type System is Sound

Sophia Drossopoulou, Susan Eisenbach, Sarfraz Khurshid

Journal Special Issue Article
Theory and Practice of Object Systems
Volume 5
Issue 1
October, 1999

A proof of the soundness of the Java type system is a first, necessary step towards demonstrating which Java programs won't compromise computer security. We consider a subset of Java describing primitive types, classes, inheritance, instance variables and methods, interfaces, shadowing, dynamic method binding, object creation, null, arrays and exception throwing and handling. We argue that for this subset the type system is sound, by proving that program execution preserves the types, up to subclasses/subinterfaces.

Distributed Software Engineering
Java Semantics
Postscript of full publication (683 kilobytes)
(need help viewing Postscript files?)
BibTEX file for the publication
Conditions for downloading publications from this site. built & maintained by Ashok Argent-Katwala.