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; Wed, 25 May 1994 12:18:45 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA12974; Wed, 25 May 1994 05:17:17 -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 AA12970; Wed, 25 May 1994 05:17:14 -0600 Received: from switha.dcs.gla.ac.uk by goggins.dcs.gla.ac.uk with LOCAL SMTP (PP) id <06916-0@goggins.dcs.gla.ac.uk>; Wed, 25 May 1994 12:17:03 +0100 Received: by switha.dcs.gla.ac.uk (4.1/Dumb) id AA11347; Wed, 25 May 94 12:16:58 BST From: tfm@dcs.gla.ac.uk Message-Id: <9405251116.AA11347@switha.dcs.gla.ac.uk> To: Konrad Slind Cc: hol2000@leopard.cs.byu.edu, tfm@dcs.gla.ac.uk Subject: Adding Type Quantification. In-Reply-To: Your message of "Tue, 24 May 94 16:17:06 +0100." <94May24.161719met_dst.8129@sunbroy14.informatik.tu-muenchen.de> Date: Wed, 25 May 94 12:16:58 +0100 Proposals for fundamental logical changes like > - hol_type: allow finer distinctions to be made, e.g., Tom > Melham's type quantification work (this would be implemented > in the datatype of terms, but direct modifications to the type > system should also be considered). always leave you open to the (basically unhelpful) suggestion "Why not just use COC (or the Nuprl logic, or system F, or whatever)". I am therefore keen to emphasize that my proposal for type quantifiers really is just an *evolutionary* improvement to the logic -- indeed, I suspect the implementation could be almost upwards-compatable. This is in keeping with the hol2000 proposal: > The time seems ripe for a HOL2000 initiative analogous to ML2000. The > goal would be to try to put together a design for the next generation > of HOL-like theorem proving environments. This should not be a > redesign from zero, but an evolution from the current state > done in a framework that does not kill off the existing HOL... Tom PS: If you liked the "first order" version of the type quantification stuff, just wait for the higher order one!