Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: tfm@dcs.gla.ac.uk
Message-Id: <9406240902.AA05661@switha.dcs.gla.ac.uk>
To: Man-Kam Mok <mok@osm7.cs.byu.edu>
Cc: info-hol@leopard.cs.byu.edu, tfm@dcs.gla.ac.uk
Subject: (deep embeddings)
In-Reply-To: Your message of "Thu, 23 Jun 94 15:29:29 MDT."
Date: Fri, 24 Jun 94 10:02:34 +0100


Man-Kam Mok asks:

>    Does anybody have experience in deep embedding a language/system inside
> HOL?  Basically, I am trying to embed a software modeling/specification
> language in HOL. Then, I could utilize the theorem proving facility in HOL to
> prove some software engineering techinques or perform verification on the
> software.

There are lots of examples of deep embeddings in HOL.  On the software side,
one example is given in the inductive definitions paper by Juanito Camilleri 
and me - it's available through my WWW page 

   http://www.dcs.glasgow.ac.uk/~tfm/

as well as being installed in the Cambridge ftp area

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

See also the past few HOL conference proceedings. There are also some
relevant papers coming up in the Malta conference.

> 	If anyone has some experience in deep embedding VHDL in HOL or other
> similar experience.  Please send me some details.  Any pointers or hints for
> papers in related subject would be helpful too.

For VHDL, you should certainly look at John van Tassel's thesis. It's
in the Cambridge ftp directory. See also the paper by Boulton et al
on embedding HDLs in HOL (same directory).  Again, there is quite a 
bit of other work.

Hope this helps,
Tom