Krivine's realizability: from storage operators to the intentional axiom of choice

International audienceWe will give a survey of some results in realizability including: * basic notions and control operators associated to Pierce's law. * the definition of data-types and storage operators (which are essential). * the interaction of intuitionistic and classical proofs to extract algorithm (illustrated by Dickson's lemma). * the use of the system clock to realize the intentional axiom of choice. We will also give a short list of open problems