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 01:39:17 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA167641958;
          Mon, 25 Sep 1995 14:45:58 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: from pelican.cs.ucla.edu by leopard.cs.byu.edu 
          with ESMTP (1.37.109.15/16.2) id AA167611956;
          Mon, 25 Sep 1995 14:45:56 -0600
Received: from localhost by pelican.cs.ucla.edu (8.6.10/UCLACS-1.0) with ESMTP 
          id MAA20398 for <info-hol@leopard.cs.byu.edu>;
          Mon, 25 Sep 1995 12:21:08 -0700
Message-Id: <199509251921.MAA20398@pelican.cs.ucla.edu>
To: info-hol@leopard.cs.byu.edu
Subject: VHDL
Date: Mon, 25 Sep 1995 12:21:07 -0700
From: Ching-Tsun Chou <chou@CS.UCLA.EDU>


Hi,

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

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

Thanks!

- Ching Tsun