Return-Path: 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, 11 Oct 1994 10:31:32 +0100 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA09259; Tue, 11 Oct 1994 03:32:39 -0600 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-request@lal.cs.byu.edu Precedence: bulk Received: from iraun1.ira.uka.de by leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA09255; Tue, 11 Oct 1994 03:32:34 -0600 Received: from i80fs2.ira.uka.de by iraun1.ira.uka.de with SMTP (PP); Tue, 11 Oct 1994 10:25:46 +0100 Received: from ira.uka.de by i80fs2.ira.uka.de id <28411-0@i80fs2.ira.uka.de>; Tue, 11 Oct 1994 10:29:13 +0100 Date: Tue, 11 Oct 94 10:29:13 EST From: reetz To: hol2000@leopard.cs.byu.edu Subject: Automating the formalization of languages in HOL Message-Id: <"i80fs2.ira.413:11.10.94.09.29.16"@ira.uka.de> One thing that can be much more automated than it currently is, is the formalization of languages in HOL, i.e. the ``deep embedding'' of languages. The idea I would to point out is that one may take a look at compiler building, where a lot of ``generating an operational semantics'', i.e. generating a compiler is automated. In contrast to that, in hol, one has currently to do almost everything by hand. A certain, implemented formalization style derived from compiler building can automate a lot of deep embedding. [dreaming:=on] Image the novice user of hol2000 just type in his well-known grammar, some rules and ``the rest'' of formalizing his language goes automatically and everything is ready to start reasoning about the language. [dreaming:=off] As a reference, I would like to hint to 1.) my paper at the last HUG 94: Reetz, Kropf: ``Simplifying deep embedding: a formalized code generator''. 2.) The library "generator" to be included in contrib of hol90.7, which is an extention of 1.): it contains the automated generation of a) a hol representation of attributed derivation trees for a supplied context--free grammar b) a hol representation of an attributation system for supplied attributation rules c) a hol representation of an code generator for supplied translation rules. Ralf. (**************************************************************) (* *) (* Ralf Reetz *) (* *) (* University of Karlsruhe *) (* Institut fuer Rechnerentwurf und Fehlertoleranz *) (* 76128 Karlsruhe, Zirkel 2, Postfach 6980, Germany *) (* *) (* e-mail: reetz@ira.uka.de *) (* WWW: http://goethe.ira.uka.de/people/reetz/reetz.html *) (* *) (**************************************************************)