Re: Subject reduction fails in Java
[This is a response to two people ...]
Carl, yes, I meant "models" of the languages Ml and Java in the sense of
physical models (ignore friction and let's study the rest). Apologies if
this causes confusion, but the point of my message remains the same.
Donald, the til & tal projects at Cornell and CMU use type information at
ALL stages of compilation/implementation. They are successful in exploiting
them. I don't think that this is an issue of theoreticians making strong
assumptions. Furthermore, it is perfectly okay to formulate models that are
good for one purpose (say, proving type soundness) and others that are good
for other purposes (say, proving a jvm implementation correct). If you do
so, you need to relate the models with (strong) adequacy theorems to ensure
that the two evaluation sequences ("executions") preserves the correct
"subject" so that your other theorems make sense. But that should be all.
Regards -- Matthias