Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
To: info-hol@leopard.cs.byu.edu, thomas@nessi.first.gmd.de
Subject: Re: hol90 version of Z?
In-Reply-To: Your message of "Mon, 04 Sep 1995 15:13:17 +0200." <95Sep4.151321met_dst.8087@sunbroy14.informatik.tu-muenchen.de>
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Date: Mon, 04 Sep 1995 17:52:03 +0100
From: Donald Syme <Donald.Syme@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:098620:950904165211"@cl.cam.ac.uk>


[ I sent this to info-hol when I was mailing to comp.specification.z,
but it hasn't appeared after three hours.  So sorry if you
get this twice. ]

> > Hello,
> >
> > does anybody know if there exists a free Z embedding in HOL90,
> > as it exists in the contrib area of HOL88 ?
> >
> > Thanks,
> > Thomas N.
>
>

I did most of the required work about 5 months ago, and will be getting
back to it after the HOL95 user's meeting.  I got as far as:
        - representing Z schemas in HOL terms (using Mike's scheme,
modified to represent schemas as abstractions, rather than terms
with free variables.  This seems a better way to go in the long run)
        - implementng pretty printing for TkHol (the graphical
interface for hol90) so schemas really look like scehmas, with
boxing, delta symbols, fonts, subterm selection and so on.
        - implementing 50% of the preterm code needed to get decent
schema entry facilities.

In the long term, I plan to do alot of work on this topic.  I
hope to implement a HOL90 Z tool as part of my PhD. thesis as an example of how
to build extended systems on top of LCF (HOL/Isabelle) theorem
provers.  The tool may incorporate an external type checker (fuzz),
and will include reasoning support for Z.  I would guess the first
usable version will be available in January of February next year - I'll
certainly be looking for beta testers if you're interested.

I hope that's of some help.

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 302521
http://www.cl.cam.ac.uk/users/drs1004/
email: Donald.Syme@cl.cam.ac.uk
-----------------------------------------------------------------------------