# How is the double negation translation similar to CPS in functional programming languages?

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.

-
Some slides of mine tackle this question. They start with a general introduction to the difference between classical and constructive mathematics and end with specific Haskell code. – Ingo Blechschmidt Jan 12 at 20:33