[TYPES] Encoding of negation

[Carter Tazio Schonwald]

I believe that this paper 
http://www.cs.bham.ac.uk/~hxt/research/effects.pdf
by Hayo Thielecke studies this style of translation and its use in the 
presence of effects
cheers,
-Carter

Philip Wadler wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> One possible encoding of negation, closely related to the CPS  
> translation, is the following:
>
>    A*         =  all Z. A+
>
>    X+         =  X
>    (A -> B)+  =  A+ -> B+
>    (not A)+   =  A+ -> Z
>
> where Z is a fresh type variable that does not appear free in A.  I  
> conjecture that
>
>    A1, ..., An |- B
>
> holds in classical logic iff
>
>    A1*, ..., An* |- B*
>
> holds in intuitionistic logic.
>
> Has anyone explored this translation?  As an example of its interest,  
> I conjecture that A* and (not (not A))* are isomorphic in the  
> presence of parametricity; this is certainly true if A contains no  
> negations.
>
> Many thanks for any responses.  Cheers,  -- P
>
>
>
>
>