Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

In Wikipedia's Double-negation translation article, I found that any formula in classical logic has its double negation as its intuitionist equivalent:

It is also possible to define φN by prefixing ¬¬ before every subformula of φ, as done by Kolmogorov. Such a translation is the logical counterpart to the call-by-name continuation-passing style translation of functional programming languages along the lines of the Curry–Howard correspondence between proofs and programs.

Could anyone explain how prefixing ¬¬ before every sub formula of a proposition is the logical counter part to call-by-name continuation-passing style? If possible, could you use Python, since I'm not familiar with Scheme and Haskell.

I've done some research into CPS, but I'm not seeing the relationship, apart from the fact that a function $P \to \bot$ doesn't have a return value.

share|improve this question

1 Answer 1

up vote 0 down vote accepted

Turns out that my question is answered in great detail here: http://www.ps.uni-saarland.de/~duchier/python/continuations.html

share|improve this answer
Can you add some commentary? I don't see any mention in that article about the correspondence between double negation and call-by-name CPS. –  Joshua Taylor Aug 25 at 19:51

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.