Tech report available: "Proving JavaS Type Soundness"

A new tech. report is now available on proving the type soundness
of a subset of the Java language, using a theorem prover
called DECLARE (influenced by PVS, Isabelle, HOL and Mizar).
The report, along with scratchy HTML versions of the 
proofs, is available at my home page


Here is the abstract:

Cambridge University Tech. Report No. 427 - "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 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.

Don Syme

At the lab:                                          At home:
The Computer Laboratory                              Trinity Hall
New Museums Site                                     CB2 1TJ
University of Cambridge                              Cambridge, UK
CB2 3QG, Cambridge, UK
Ph: +44 (0) 1223 334688                              Ph: +44 (0) 1223 505863
email: drs1004@cl.cam.ac.uk