Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from antares.mcs.anl.gov (actually antares9.mcs.anl.gov !OR! owner-qed@mcs.anl.gov) 
          by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk;
          Thu, 25 Aug 1994 01:10:39 +0100
Received: from localhost (listserv@localhost) 
          by antares.mcs.anl.gov (8.6.4/8.6.4) id TAA01860 for qed-out;
          Wed, 24 Aug 1994 19:06:01 -0500
Received: from oracorp.com (scylla.oracorp.com [192.76.175.102]) 
          by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id TAA01855 
          for <qed@mcs.anl.gov>; Wed, 24 Aug 1994 19:05:54 -0500
From: hoove@oracorp.com
Received: from euterpe.oracorp.com by oracorp.com (4.1/2.1-ORA Corporation) 
          id AA03048; Wed, 24 Aug 94 20:04:05 EDT
Date: Wed, 24 Aug 94 20:04:04 EDT
Received: by euterpe.oracorp.com (4.1/1.3-ORA Corporation) id AA01946;
          Wed, 24 Aug 94 20:04:04 EDT
Message-Id: <9408250004.AA01946@euterpe.oracorp.com>
To: qed@mcs.anl.gov
Subject: Re: Types and sorts
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

farmer@linus.mitre.org writes:

  There is a distinction between "types" and "sorts" in the IMPS logic
  (officially named LUTINS) that might be helpful to the recent
  discussion about type theory vs. set theory.

  etc.  

I wonder if he would be willing to compare the type theory of IMPS to
that of PVS.  In PVS, types are closed under subtypes (any predicate
defines a subtype of a type) so it appears that 

  PVS-type = IMPS-(type or sort)

I prefer PVS because I don't see the advantage of distinguishing types
and sorts.  Am I missing something?

Doug Hoover
hoove@oracorp.com