[Haskell-cafe] Tutorial: Curry-Howard Correspondence

[Iavor Diatchki]

Hello,

On 10/17/07, Lennart Augustsson <lennart at augustsson.net> wrote:
> Check Wikipedia.  Peirce law, law of excluded middle, double negation, ...
> they are all equivalent and it can be instructive to see how one can derive
> one from the other.

Apparently these axioms are not all equivalent (I was quite surprised
to learn that :-).  Here is some interesting---but perhaps a bit
advanced for a tutorial on CH---reading which studies the relation
between classical logic and computation:
http://coq.inria.fr/~herbelin/publis/icalp-AriHer03-minimal-classical.ps.gz

-- 
Iavor