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; Tue, 26 Sep 1995 11:21:33 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA004708856;
          Tue, 26 Sep 1995 03:47:36 -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 AA004678824;
          Tue, 26 Sep 1995 03:47:04 -0600
Received: from gozo.dcs.gla.ac.uk by vanuata.dcs.gla.ac.uk with LOCAL SMTP (PP);
          Tue, 26 Sep 1995 10:35:56 +0100
To: Ching-Tsun Chou <chou@cs.ucla.edu>
Cc: info-hol@leopard.cs.byu.edu, tfm@dcs.gla.ac.uk
Subject: Re: VHDL
In-Reply-To: Your message of "Mon, 25 Sep 1995 12:21:07 PDT." <199509251921.MAA20398@pelican.cs.ucla.edu>
Date: Tue, 26 Sep 1995 10:35:53 +0100
From: Tom Melham <tfm@dcs.gla.ac.uk>
Message-ID: <"swan.cl.cam.:133920:950926102304"@cl.cam.ac.uk>

> Where can I get a copy of John Van Tassel's work on
> formalizing VHDL in HOL?

John's work is available by ftp from:

  ftp://ftp.cl.cam.ac.uk/hvg/papers

an html interface is available via

  http://www.cl.cam.ac.uk/Research/HVG/FTP/FTP.html

See also the following -- hot off the press!

   R. Reetz, `Deep Embedding VHDL', in Higher Order Logic Theorem Proving
   and Its Applications: 8th International Workshop, Aspen Grove, Utah,
   September 1995: Proceedings, edited by E. T. Schubert, P. J. Windley,
   and J. Alves-Foss, Lecture Notes in Computer Science, Volume 971
   (Springer-Verlag, 1995), pp. 277-292.

> Also, are there other works on formalizing VHDL in
> other theorem provers?

Yes.  I believe that some work has been done with the Boyer-Moore system,
among others.  Can anyone be more precise?

Tom