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; Thu, 23 Jun 1994 22:44:44 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA08090;
          Thu, 23 Jun 1994 15:35:10 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from osm5.cs.byu.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA08086;
          Thu, 23 Jun 1994 15:35:09 -0600
Received: by osm7.cs.byu.edu (1.37.109.10G/16.2) id AA270316969;
          Thu, 23 Jun 1994 15:29:29 -0600
Date: Thu, 23 Jun 1994 15:29:29 -0600
From: Man-Kam Mok <mok@osm7.cs.byu.edu>
To: info-hol@leopard.cs.byu.edu
Message-ID: <"swan.cl.cam.:205780:940623214526"@cl.cam.ac.uk>

	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.

	The system that I try to embedded is Object-Oriented System Modeling,
OSM.  It support both graphical and textual representation of the specification.Moreover, both its semantics and syntax have a formal definition.  Thus, we 
could be able to prove that certain engineering techinques give certain
properties in the software.

	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.

	Man-Kam Mok
	mok@osm7.cs.byu.edu