[Prev][Next][Index][Thread]
Re: Subject reduction fails in Java
Date: Sun, 21 Jun 1998 19:01:38 -0500 (CDT)
From: Matthias Felleisen <matthias@cs.rice.edu>
[------- The Types Forum ------ http://www.cs.indiana.edu/types -------]
Dear All:
Before you jump on Java or the typing rules, you may wish to consider the
*full* context of the discussion.
Java is *not* a functional language. It is an imperative language and, if
we wish to prove all of Java type sound, we should include assignment in
the reduction semantics. Felleisen-Friedman-Hieb (popl 87, tcs 87, 89) have
shown that this strategy is possible. Felleisen-Wright (rice 91/info-comp
94) have shown how to prove type-soundness for core ML. At POPL'98,
Perhaps you mean that type-soundness was proved for an idealized
language containing key constructs like those of core ML. Proving
type-soundness of core ML is a completely different task.
Flatt-Krishnamurthi-Felleisen show how to scale this approach to
Java. Proving type soundness of Java + if-expressions using small-step
subject-reduction is then straightforward.
Do you mean Java or an idealized language with key contructs like
those of Java? The Java definition is a big fat book with hundreds of
constructs. A written-out proof of its soundness would probably be at
least that long even if it didn't include the formalization itself.
Follow-Ups: