Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Date: Mon, 13 Mar 95 10:55:33 EST
From: reetz <reetz@ira.uka.de>
To: info-hol@leopard.cs.byu.edu
Cc: Richard.Boulton@cl.cam.ac.uk, shaw@cs.ucdavis.edu
Subject: new version of library generator available
Message-Id: <"i80fs2.ira.634:13.03.95.09.55.35"@ira.uka.de>

Dear all,
I'm glad to announce that a new version of the library "generator"
for simplifying deep embedding by generating formal compiler in HOL
is now available.

from the README/CHANGES:

This is the library "generator" Version 2.0, which simplifies the 
formalisation method ``deep embedding'' for a system with syntax and semantics
in the following way: a formalisation of the syntax described by a 
context--free grammar is automatically generated and a formalisation of the
complete semantics for the given syntax is simplified by automatically
generating an attributation system and a formal code generator out of a
formalised context--restricted semantics.

For references, see 

@inproceedings{ReKr94b,
  author      ={{R. Reetz} and {Th. Kropf}},
  title       ={Simplifying Deep Embedding: A Formalised Code Generator},
  booktitle   ={Proc. of the International Workshop on Higher Order Logic
                Theorem Proving and its Applications},
  year        ={1994},
  editor      ={},
  pages       ={378--390},
  organization={},
  publisher   ={Lecture Notes in Computer Science No. 859, Springer},
  address     ={Malta},
  month       ={September},
  note        ={},
  key         ={ReKr94b}
}

and see the supplied document whose reference is

@techreport{Reet95a,
  author      ={R. Reetz},
  title       ={Simplifying Deep Embedding: Generating Formal Compilers
                in HOL. Version 2.0},
  institution ={Sonderforschungsbereich 358, Universit\"{a}t Karlsruhe},
  year        ={1995},
  type        ={Technical Report},
  number      ={SFB358-C2-1/95},
  address     ={Germany},
  month       ={March},
  note        ={},
  key         ={Reet95a}
}

This library "generator" is for HOL90.7 and is assumed to be installed
in the contrib directory of your HOL90.7 installation. You need the libraries
"mutrec" and "more_utils". Furthermore, you need the sml/nj library
version 0.2. There are no help files available yet. Take a look at the 
examples. Bug reports and other comments are welcome.

In order to be able to use all features supplied with this library, you
need the graph visualization daVinci 1.4.2. For information on daVinci, see
on WWW with:
http://www.informatik.uni-bremen.de/~inform/forschung/daVinci/daVinci.html
However, this library does not need daVinci in order to be used.

Version 2.0

- The structure of the library has completely been changed. Now, generation
  of 1) derivation trees, 2) attributation and translation and 3) proving
  functions has been divided into seperate functors.

- Sereval bugs on reporting errors fixed. You can't handle a functor, thus
  a raised HOL_ERR by the functors of the generator does not make a lot of
  sense. Instead, own exceptions with error messages reported to std_out
  have been implemented.

- Derivation trees can now be written into a file format fitting for
  daVinci 1.4.2 in order to get a visualization of attributation phases.
  Useful for debugging attributation rules.

- Documentation has been improved a lot.


The libraries generator and more_utils are available via WWW:

http://goethe.ira.uka.de/hvg/software.html

or via ftp:

goethe.ira.uka.de  in /pub/software/generator/ and /pub/software/more_utils/


hope this helps,
Ralf.

(*******************************************************************)
(*                                                                 *)
(*  Ralf Reetz                                                     *)
(*                                                                 *)
(*  University of Karlsruhe                                        *)
(*  Institut fuer Rechnerentwurf und Fehlertoleranz                *)
(*  76128 Karlsruhe, Zirkel 2, Postfach 6980, Germany              *)
(*                                                                 *)
(*  e-mail: reetz@informatik.uni-karlsruhe.de or reetz@ira.uka.de  *)
(*  WWW:    http://goethe.ira.uka.de/people/reetz/reetz.html       *)
(*                                                                 *)
(*******************************************************************)