[TYPES] Limited use of negation types?

Alain Frisch Alain.Frisch at inria.fr
Fri Dec 23 10:17:13 EST 2005

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).


The paper is rather dense. Let me know if you want more information.

-- Alain

More information about the Types-list mailing list