Don Syme: Proving Java Type Soundness. Formal Syntax and Semantics of Java 1999: 83-118