Department of Computer Science and Technology

Technical reports

Proving Java type soundness

Don Syme

June 1997, 35 pages

DOI: 10.48456/tr-427

Abstract

This technical report describes a machine checked proof of the type soundness of a subset of the Java language called Java_s. A formal semantics for this subset has been developed by Drossopoulou and Eisenbach, and they have sketched an outline of the type soundness proof. The formulation developed here complements their written semantics and proof 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.

Full text

PDF (2.4 MB)

BibTeX record

@TechReport{UCAM-CL-TR-427,
  author =	 {Syme, Don},
  title = 	 {{Proving Java type soundness}},
  year = 	 1997,
  month = 	 jun,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-427.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-427},
  number = 	 {UCAM-CL-TR-427}
}