First, we will look at programs extracted from proofs of the infinite tape lemma (also called Stolzenberg's principle, which says that a partition of N in two has at least one infinite part). We will show how a specific axiom on streams allow the extraction of an efficient program.

Using this first program, we will extract programs for Ramsey theorem (not only for pairs) and as an application, we will get a program for the ``happy ending problem'' (for all N, in any infinite set of points, we can find N points which are the vertices of a convex polygon).

All those extracted programs are SML program using CallCC. To prove that those SML programs are indeed correct, we will introduce call-by-value realizability and see that it is a promising variation of classical realizability.