L'isomorphisme de Curry-Howard permet d'associer à toute preuve intuitionniste convenablement formalisée un lambda-terme représentant un programme. Le problème de la spécification est alors de déterminer l'ensemble des programmes associées aux preuves d'un formule donnée. On connait de nombreux cadres dans lesquels ce problème est résolu (Arithmétiques intuitionniste du second ordre par exemple). Nous essaierons d'étudier ce qui se passe lorsque l'on étend l'isomorphisme de Curry-Howard à la logique classique. Il faudra pour cela généraliser un outil puissant: la réalisabilité. Nous appliquerons ensuite cela à la logique du second ordre avec axiome du choix.