Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Wed, 4 Nov 1992 16:44:18 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA05369; Wed, 4 Nov 92 08:16:13 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from nene.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA05364; Wed, 4 Nov 92 08:15:59 -0800 Received: from guillemot.cl.cam.ac.uk (user tfm (OK)) by nene.cl.cam.ac.uk with SMTP (PP-6.3) to cl; Wed, 4 Nov 1992 16:15:03 +0000 To: info-hol@edu.uidaho.cs.ted Cc: Tom.Melham@uk.ac.cam.cl Subject: paper on type quantifiers. Date: Wed, 04 Nov 92 16:15:46 +0000 From: Tom Melham Message-Id: <"nene.cl.ca.731:04.11.92.16.15.05"@cl.cam.ac.uk> I have made my paper on quantification over type variables in HOL available by ftp from ftp.cl.cam.ac.uk in the directory hvg/papers. The relevant file is called TypeQuantifiers.ps.Z. The details are: The HOL Logic Extended with Quantification over Type Variables Tom Melham ABSTRACT. This paper discusses a proposal to extend the primitive basis of the HOL logic with a very simple form of quantification over types. It is shown how certain practical problems with using the definitional mechanism of HOL would be solved by the additional expressive power gained by making this extension. Tom