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