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.
Turns out that my question is answered in great detail here: http://www.ps.uni-saarland.de/~duchier/python/continuations.html