Re: Types and sorts
Wed, 24 Aug 94 20:04:04 EDT 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.


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