ExtendedStaticChecking for JavaLanguage

See

http://secure.ucd.ie/products/opensource/ESCJava2/

http://secure.ucd.ie/products/opensource/ESCJava2/ESCTools/docs/ESCJAVA-UsersManual.html

For an ''idea'' how this works see ProofAnnotationsForBubbleSort.

There seem to be versions for Modula 3 and Haskell now:
* http://lambda-the-ultimate.org/node/1689 -> http://www.cl.cam.ac.uk/~nx200/research/escH-hw.ps

For a general review see http://radu.ucd.ie/hp/papers/phd.pdf
----
CategoryLanguageTyping