Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Wed, 7 Jun 1995 14:16:28 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA014379302;
          Wed, 7 Jun 1995 06:48:22 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: from vanuata.dcs.gla.ac.uk by leopard.cs.byu.edu 
          with ESMTP (1.37.109.15/16.2) id AA014299257;
          Wed, 7 Jun 1995 06:47:37 -0600
Received: from gozo.dcs.gla.ac.uk by vanuata.dcs.gla.ac.uk with LOCAL SMTP (PP);
          Wed, 7 Jun 1995 13:47:12 +0100
To: Mike Coe <coe@sctc.com>
Cc: info-hol@leopard.cs.byu.edu, tfm@dcs.gla.ac.uk
Subject: Re: software spec
In-Reply-To: Your message of "Mon, 05 Jun 1995 14:03:28 CDT." <199506051903.OAA03660@arcadia.sctc.com>
Date: Wed, 07 Jun 1995 13:46:57 +0100
From: Tom Melham <tfm@dcs.gla.ac.uk>
Message-ID: <"swan.cl.cam.:143680:950607131816"@cl.cam.ac.uk>

> while there are numerous examples of hardware
> specification and verification in HOL, I know
> of little in the area of software specification.
> 
> since I have not been following HOL to closely
> for about a year now, could someone point to
> some good examples of this.

There are numerous examples of using HOL to specify and reason about
software and programming languages.  A good way into this work is
to have a look at the proceedings of the past few HOL meetings:

       Thomas F Melham and Juanito Camilleri, eds 
       Higher Order Logic Theorem Proving and its Applications: 
       6th International Workshop, Valletta, Malta, 19-22 September 
       1994: Proceedings, Lecture Notes in Computer Science 
       (Springer-Verlag, 1994).

       Jeffrey J  Joyce and Carl-Johan H Seger, eds 
       Higher Order Logic Theorem Proving and its Applications: 
       6th International Workshop, HUG'93,
       Vancouver, B.C., August 11-13 1993: Proceedings,
       Lecture Notes in Computer Science, 780 (Springer-Verlag, 1994).

       L J M Claesen and M J C Gordon, eds.
       Higher Order Logic Theorem Proving and its Applications: 
       Proceedings of the IFIP TC10/WG10.2 
       International Workshop, Leuven, September 1992,
       IFIP Transactions A-20 (North-Holland, 1993).

       M Archer, J J Joyce, K N Levitt, and P J Windley, eds.
       Proceedings of the 1991 International Workshop
       on the HOL Theorem Proving System and its Applications,
       Davis, August 1991 (IEEE Computer Society Press, 1992).

       G. Winskel, ed 
       Proceedings of the Third HOL Users Meeting: Aarhus, October 1990,
       Report DAIMI PB-340, 
       Computer Science Department, Aarhus University
       (December 1990).

There are also some relevant papers in a soon-to-appear issue of The Computer
Journal.  See

      http://www.oup.co.uk/oup/smj/journals/ed/titles/computer_journal/docs/journal_contents/Volume_38_Number_2/

Tom