[TYPES] Limited use of negation types?
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
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.
More information about the Types-list