From owner-qed Wed Aug 24 19:06:44 1994
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