Raffalli describes a strategy that constructs programs from proofs. The formula of interest is of the form ∀ x (I[x] → ∃ y ( O[y] ∨ S [x,y] ) ).

O is assumed to be a data type, while S is assumed to be a decidable predicate. The author uses mixed second order logic to obtain the results of the paper. It is shown that, from a formula of the above form, one can construct a set of &lgr;-terms, each of which reduces to a closed &lgr;-term, which can be used to construct a value for interpreting the variable symbol y that satisfies the formula S.

In contrast to other approaches, the author uses a Gödel transformation to transform classical proofs of a formula into intuitionistic ones (which is necessary in order to obtain specific values of variables y that are bound by a binding of the form ∃ y).

The construction is an improvement over the method that consists of trying out all possible solutions (which is applicable here, since S is assumed to be decidable). This is illustrated in an example that uses a proof of Dickson’s lemma, where one can see that the number of values to be tested is far smaller than the maximum possible number (which is determined by the number of subsets, and therefore is exponential). So, the improvement is quite impressive.