[Prev][Next][Index][Thread]
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
http://www.cl.cam.ac.uk/users/drs1004
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.
Yours,
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
http://www.cl.cam.ac.uk/users/drs1004/
email: drs1004@cl.cam.ac.uk
-----------------------------------------------------------------------------