Return-Path: Delivery-Date: Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 25 Aug 1993 16:43:54 +0100 Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA02324; Wed, 25 Aug 93 08:37:29 -0700 Sender: info-hol-request@cs.uidaho.edu Errors-To: info-hol-request@cs.uidaho.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.4/16.2) id AA02320; Wed, 25 Aug 93 08:37:27 -0700 Received: from albatross.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Wed, 25 Aug 1993 16:37:06 +0100 To: info-hol@dworshak.cs.uidaho.edu Subject: HOL improvement survey Date: Wed, 25 Aug 93 16:36:56 +0100 From: John Harrison Message-Id: <"swan.cl.cam.:216540:930825153721"@cl.cam.ac.uk> As promised at the Vancouver meeting, I'm organizing a survey to collect views on how the HOL system should be improved. I make no restrictions on the types of suggestions, so all the following are reasonable: * SKOLEM_CONV should fail on exists terms * SUBST shouldn't be a primitive inference rule * HOL should have a proof editor like Nuprl's * HOL should have dependent types Please email suggestions to me, jrh@cl.cam.ac.uk. If you'd like an acknowledgement, say so explicitly; otherwise I'll simply collate the replies and summarize in a couple of weeks or so. I don't anticipate including individuals' names in the summary, but tell me anyway if you really want your comments to be anonymous. Finally, I should add that we are not committed to accommodating any of the suggestions, but will certainly consider them. John.