[Date Prev][Date Next] [Chronological] [Thread] [Top]

[no subject]

> 
> I forward a part of a message that John Harrison sent me.
> 
> ---------- Forwarded message ----------
> Date: Fri, 27 Jun 1997 21:55:04 +0100
> From: John Harrison <John.Harrison@cl.cam.ac.uk>
> To: Andrzej Trybulec <trybulec@math.uw.bialystok.pl>
> 
> ...........
> P.S. If you haven't already seen them, you might like to glance at a couple
> of Cambridge technical reports that are markedly Mizar-inspired:
> 
>   http://www.cl.cam.ac.uk/users/jrh/papers/style.html
> 
>   http://www.cl.cam.ac.uk/users/drs1004/reports/declare.ps

You may also be interested in 
   http://www.cl.cam.ac.uk/users/drs1004/reports/java.ps

which describes the use of DECLARE to prove the type soundness
property of a significant subset of the Java langauge.
The specifications and proof scripts are available from
my home page at
   http://www.cl.cam.ac.uk/users/drs1004

Cheers,
Don

-----------------------------------------------------------------------------
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
-----------------------------------------------------------------------------