Proving Java Type Soundness

This technical report describes a machine checked proof of the type soundness of a subset of the Java language called Javas. A formal semantics for this subset has been develooped by Drossopoulou and Eisenbach, and they have sketched an outline of the type soundness proof. The formulation developed here complements their written semantics and proff by correcting and clarifying significant details; and it demonstrates the utility of formal, machine checking when exploring a large and detailed proof based on operational semantics. The development also serves as a case study in the application of ‘declarative’ proof techniques to a major property of an operational system.