Proving Java Type Soundness

Abstract

This chapter describes a machine checked proof of the type soundness of a subset of Java (we call this subset Javatex2html_wrap_inline102). 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.