[Prev][Next][Index][Thread]

ftp and URL location of the Java soundness paper


[------ 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 
        http://src.doc.ic.ac.uk/public/ic.doc/ALA/papers/S.Drossopoulou/

It can  also be reached from the ftp site:
        ftp site:       santos.doc.ic.ac.uk
        directory:      /vol/ftp/pub/papers/S.Drossopoulou
        file:           JavaSound.ps

We are looking forward to feedback and comments.

Regards,

Sophia Drossopoulou  and Susan Eisenbach, Imperial College 
        http://www-ala.doc.ic.ac.uk/~scd/
        and 
        http://www-dse.doc.ic.ac.uk/cgi-bin/show_user?sue+Ms._S._Eisenbach

Abstract
========
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
type system.