Soundness of the C++ or Java type system

[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]

Does anybody know of any formal proofs, or informal arguments
that show that C++ or Java have a sound type system?

If I get any replies, I will compile the answers and post
on this news group.

Thanks in advance,

Sophia Drossopoulou,
Imperial College,