Computing Publications

Publications Home » Is the Java Type System Sound?

Is the Java Type System Sound?

Sophia Drossopoulou, Susan Eisenbach

Conference or Workshop Paper
FOOL 4( Foundations of Object Oriented Languages), Paris

We give an operational semantics for a large 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 build a model that is simple and near the programmer's intuition. We distinguish between three languages: Javas is the original language. Javase is an enriched version of Javas containing compile time information necessary for execution. Javar is an extended version of Javase allowing for runtime constructs such as addresses.

We give a type system for Javas, Javase and Javar. The two latter are slight modifications of the former. We prove that well-typed Javas terms retain their type when the corresponding Javase or Javar term is considered. The operational semantics describes the execution of Javar terms for given Javase programs. We prove a subject reduction theorem, which states that execution of Javar preserves types, up to subclasses/subinterfaces

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