A program for the full axiom of choice

The theory of classical realizability is a framework for the Curry-Howardcorrespondence which enables to associate a program with each proof inZermelo-Fraenkel set theory. But, almost all the applications of mathematics inphysics, probability, statistics, etc. use Analysis i.e. the axiom of dependentchoice (DC) or even the (full) axiom of choice (AC). It is therefore importantto find explicit programs for these axioms. Various solutions have been foundfor DC, for instance the lambda-term called "bar recursion" or the instruction"quote" of LISP. We present here the first program for AC