The Curry-Howard isomorphism between mathematical proofs and computer programs, initially limited to a purely functional notion of computations and intuitionistic logic, has been extended since then to new programming paradigms including computational features such as control operators. Interestingly, the addition of control operators to a programming language corresponds, through Curry-Howard isomorphism, to the addition of the principle of excluded-middle to the logic. This phenomenon is not isolated: adding axioms to a logical system correspond to the addition of computing primitives to a programming language. To be able to reason on more expressive programming languages, it is necessary to find the axioms that the corresponding logic should satisfy. Dually, studying the computational counterpart of a given axiom has shown to be particularly fruitful. We propose to apply this methodology to choice principles, that are ubiquitous in mathematics. The full axiom of choice has been deeply studied in numerous works in mathematics and can be expressed in different ways. Even though these variants are equivalent in a classical system (that is in a logic including the excluded-middle), this is no longer the case in a constructive setting. For instance, under common assumptions, the usual axiom of choice (in terms of quotient sets) is known to entails the law of excluded-middle, itself incompatible with many constructive settings. We can thus affirm that constructive theories do not capture the true nature and full strength of the axiom of choice. One of the mid-term goal of this project is then to wonder: what is the computational interpretation of the axiom of choice? This question actually stands for several restricted form of choices, such as König's lemma, whose importance has been emphasized by the program of reverse mathematics. This project can be seen as a first step to pave the way towards a computational point of view on constructive reverse mathematics.