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.