Technical reports
Proving Java type soundness
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} }