[TYPES] Limited use of negation types?

[Giuseppe Castagna]

Alain Frisch wrote:
 > I'm pretty sure this is not what you have in mind, but my LICS 2002
 > paper _Semantic Subtyping_ describes a type system with a classical
 > (set-theoretic interpretation) of negation types. The negation of (t ->
 > s) is just the set of values which are not of type (t -> s), where the
 > type of an abstraction is explicitly given in its prototype (and cannot
 > change during evaluation).
 >
 > http://www.cduce.org/papers/lics02.ps.gz
 >
 > The paper is rather dense. Let me know if you want more information.
 >
 > -- Alain

If you want less a dense paper, actually an introduction to the paper Alain 
cited above, you can check one of this year's ICALP/PPDP joint invited talks:

A Gentle Introduction to Semantic Subtyping

by Alain and myself and included in the PPDP 2005 proceedings. You can also find 
it here.

http://www.di.ens.fr/users/castagna/papers/icalp-ppdp05.pdf

Cheers

---Beppe---