Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu by nene.cl.cam.ac.uk with SMTP (PP-6.4);
          Thu, 26 May 1994 17:43:44 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA25831;
          Thu, 26 May 1994 10:39:57 -0600
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
Received: from cornell.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) 
          id AA25827; Thu, 26 May 1994 10:39:56 -0600
Received: from msiadmin.cit.cornell.edu ([128.253.216.2]) by cornell.edu 
          with SMTP id <581346-2>; Thu, 26 May 1994 12:40:05 -0400
Date: Thu, 26 May 1994 12:39:46 -0400
From: garrel@msiadmin.cit.cornell.edu (Garrel Pottinger-MSI Visitor)
Received: from msipawn.409col_ave by msiadmin.cit.cornell.edu (4.1/1.5) 
          id AA13644; Thu, 26 May 94 12:39:46 EDT
Message-Id: <9405261639.AA13644@msiadmin.cit.cornell.edu>
To: hol2000@leopard.cs.byu.edu, mel@ultrastar.EE.CORNELL.EDU
Subject: Re: assumption numbering, user interfaces ...

Miriam Leeser suggests that it would be good to have a richer set of types
to work with.  Those who are of like mind should take a look at my paper
"A Classical Type Theory with Transfinite Types" (reference appended).
The types of the system described there --- CT^3 (Classical Transfinite
Type Theory) --- includes dependent products and climbs a LONG way up the
ladder of abstraction.  Also, although I haven't written this up for
publication, I know how to add sums, including infinite sums.

Regards,

Garrel

**********************************************************************

@incollection{pottinger:classical,
      author = "Garrel Pottinger",
      title = "A Classical Type Theory with Transfinite Types",
      booktitle = "Higher Order Logic Theorem Proving and its Applications",
      editor = "Luc {J.} {M.} Claesen and Michael {J.} {C.} Gordon",
      publisher = "North-Holland",
      year = 1993,
      pages = "81--94"
}