Don Syme. Proving Java Type Soundness. In Jim Alves-Foss, editor, Formal Syntax and Semantics of Java. Volume 1523 of Lecture Notes in Computer Science, pages 83-118, Springer, 1999. [doi]
This chapter describes a machine checked proof of the type soundness of a subset of Java (we call this subset JavaS). In Chapter 3, a formal semantics for approximately the same subset was presented by Drossopoulou and Eisenbach. The work presented here serves two roles: it complements the written semantics by correcting and clarifying some details; and it demonstrates the utility of formal, machine checking when exploring a large and detailed proof based on operational semantics.1 This work contributes to three distinct fields of formal reasoning:
The Formal Study of Java: We contribute a detailed analysis of a significant property of Java, and provide corrections to proofs that are interesting in their own right.
Tools for Formal Methods: This work is a major case study in so-called ‘declarative’ proof techniques. The tool we use, called DECLARE [Sym97], has been developed by the author to demonstrate the utility of these techniques.
Formally Checked Properties of Languages: This work contributes a tool and a methodology for the general task of machine checking properties of languages.
Most of this chapter should be clear to readers with a basic understanding of operational semantics, formal specification and the results presented in Chapter