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; Fri, 27 May 1994 13:00:11 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA03225; Fri, 27 May 1994 05:57:02 -0600 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-request@lal.cs.byu.edu Precedence: bulk Received: from vanuata.dcs.gla.ac.uk by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA03221; Fri, 27 May 1994 05:57:00 -0600 Received: from switha.dcs.gla.ac.uk by goggins.dcs.gla.ac.uk with LOCAL SMTP (PP) id <11445-0@goggins.dcs.gla.ac.uk>; Fri, 27 May 1994 12:56:29 +0100 Received: by switha.dcs.gla.ac.uk (4.1/Dumb) id AA15502; Fri, 27 May 94 12:56:27 BST From: tfm@dcs.gla.ac.uk Message-Id: <9405271156.AA15502@switha.dcs.gla.ac.uk> To: hol2000@leopard.cs.byu.edu Cc: tfm@dcs.gla.ac.uk Subject: More Tools - Syntax. Date: Fri, 27 May 94 12:56:27 +0100 I am working with Andy Gordon on some ideas for tools for constructing deep embeddings of syntaxes with variable binding. This is a real pain to do by hand (believe me!) so some good tools here would be very useful indeed. I believe well-designed tools of this kind are very important. Consider, for example, the recursive types package. Before that came along, the HOL community was pretty much stuck with the natural numbers, functions, and lists. Many people either didn't know how to construct new types, or were unwilling to do the necessary hand proofs. So the package was an enabling technology, as well as a very effective productivity-increasing one. We need more of the same. (We also need other forms of automation, too, of course). Tom