[TYPES] Limited use of negation types?

[Neelakantan Krishnaswami]

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
 > pointers?

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

-- 
Neel Krishnaswami
neelk at cs.cmu.edu