ftp and URL location of the Java soundness paper
Subject: ftp and URL location of the Java soundness paper
From: Sophia Drossopoulou <email@example.com>
Date: Tue, 22 Oct 96 18:18 BST
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
I apologize for giving incomplete information yesterday.
Our paper on the Java type system is at
It can also be reached from the ftp site:
ftp site: santos.doc.ic.ac.uk
We are looking forward to feedback and comments.
Sophia Drossopoulou and Susan Eisenbach, Imperial College
We argue that the Java type system is sound, by proving a subject
reduction theorem. We define a subset of Java, a language which is safe and
which reflects the most essential features of Java, a term rewriting system
for the operational semantics and a type inference system to describe compile
time type checking. We prove that program execution preserves the types, up
to the subclass/subinterface relationship.
In this paper we consider the following parts of the
Java language: primitive types, classes and inheritance, instance
variables and instance methods, interfaces, shadowing of instance variables,
and dynamic method binding. We plan to extend our study, starting with arrays
and the associated dynamic checks, until we either have covered all of
Java -- or we have uncovered loopholes in the