[TYPES] Limited use of negation types?

[Alain Frisch]

Jim Apple wrote:
> [The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]
> 
> I recall seeing somewhere a paper on the limited use of classical logic
> in functional programming, that somehow negation types had an
> interpretation under certain circumstances.
> 
> I know I downloaded the paper, but I don't know where I put it. ANy
> pointers?


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