Type Soundness is about proving safety invariants of abstract machines that arise from certain static checks, such as type checking. In the late 1990s there was a lot of research activity into using interactive theorem provers to help prove type soundness properties of abstract models of programming languages. My main work in this field was to prove type soundness for a subset of Java, using my theorem prover DECLARE. This work is best documented in my PhD thesis. An old version of the specifications and proofs are available online.