[TYPES] Limited use of negation types?
neelk at gs3106.sp.cs.cmu.edu
Fri Dec 23 02:24:29 EST 2005
Jim Apple writes:
> [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
You might want Griffin's paper "A Formulae-as-Types Notion of Control"
describes how the type of call/cc can be interpreted as Peirce's law
(a variant formulation of excluded middle).
Or you might want Parigot's "Lambda-Mu Calculus: an Alogrithmic
Interpretation of Classical Natural Deduction".
neelk at cs.cmu.edu
More information about the Types-list