Curry-Howard and programs from non-constructive proofs This is a follow up question to 

What is the difference between proofs and programs (or between propositions and types)?

What program would correspond to a non-constructive (classical) proof of the form $\forall k \ T(e,k) \lor \lnot \forall k \ T(e,k)$? (Assume that $T$ is some interesting decidable relation e.g. $e$-th TM does not halt in $k$ steps.)

(ps: I am posting this question partly because I am interested in learning more about what Neel means by "the Godel-Gentzen translation is a continuation-passing transformation" in his comment.)
This an interesting question. Obviously one can't expect to have a program that decides for each $e$ whether $\forall k T(e, k)$ holds or not, as this would decide the Halting Problem. As mentioned already, there are several ways of interpreting proofs computationally: extensions of Curry-Howard, realizability, dialectica, and so on. But they would all computationally interpret the theorem you mentioned more or less in the following way.

For simplicity consider the equivalent classical theorem

(1) $\exists i \forall j (\neg T(e, j) \to \neg T(e, i))$

This is (constructively) equivalent to the one mentioned because given $i$ we can decide whether $\forall k T(e, k)$ holds or not by simply checking the value of $\neg T(e, i)$. If $\neg T(e, i)$ holds then $\exists i \neg T(e, i)$ and hence $\neg \forall i T(e, i)$. If on the other hand $\neg T(e, i)$ does not hold then by (1) we have $\forall j (\neg T(e, j) \to \bot)$ which implies $\forall j T(e, j)$. 

Now, again we can't compute $i$ in (1) for each given $e$ because we would again solve the Halting Problem. What all interpretations mentioned above would do is to look at the equivalent theorem

(2) $\forall f \exists i&#39; (\neg T(e, f(i&#39;)) \to \neg T(e, i&#39;))$

The function $f$ is called the Herbrand function. It tries to compute a counter example $j$ for each given potential witness $i$. It is clear that (1) and (2) are equivalent. From left to right this is constructive, simply take $i&#39; = i$ in (2), where $i$ is the assumed witness of (1). From right to left one has to reason classically. Assume (1) was not true. Then, 

(3) $\forall i \exists j \neg (\neg T(e, j) \to \neg T(e, i))$ 

Let $f&#39;$ be a function witnessing this, i.e. 

(4) $\forall i \neg (\neg T(e, f&#39;(i)) \to \neg T(e, i))$ 

Now, take $f = f&#39;$ in (2) and we have $(\neg T(e, f&#39;(i&#39;)) \to \neg T(e, i&#39;))$, for some $i&#39;$. But taking $i = i&#39;$ in (4) we obtain the negation of that, contradiction. Hence (2) implies (1).

So, we have that (1) and (2) are classically equivalent. But the interesting thing is that (2) has now a very simple constructive witness. Simply take $i&#39; = f(0)$ if $T(e, f(0))$ does not hold, because then the conclusion of (2) is true; or else take $i&#39; = 0$ if $T(e, f(0))$ holds, because then $\neg T(e, f(0))$ does not hold and the premise of (2) is false, making it again true.

Hence, the way to computationally interpret a classical theorem like (1) is to look at a (classically) equivalent formulation which can be proven constructively, in our case (2). 

The different interpretations mentioned above only diverge on the way the function $f$ pops up. In the case of realizability and the dialectica interpretation this is explicitly given by the interpretation, when combined with some form of negative translation (like Goedel-Gentzen's). In the case of Curry-Howard extensions with call-cc and continuation operators the function $f$ arises from the fact that the program is allowed to "know" how a certain value (in our case $i$) will be used, so $f$ is the continuation of the program around the point where $i$ is computed.

Another important point is that you want the passage from (1) to (2) to be "modular", i.e. if (1) is used to prove (1'), then its interpretation (2) should be used used in similar way to prove the interpretation of (1'), say (2'). All the interpretations mentioned above do that, including the Goedel-Gentzen negative translation.