Cette thèse s'intéresse à la correspondance de Curry-Howard classique et son interaction avec le forcing de Cohen, en s'appuyant sur les outils de la réalisabilité classique. Dans une première partie, nous commençons par une introduction générale à la réalisabilité classique dans PA2, avec pour fil directeur l'extraction de témoin. Cette introduction couvre la description de la machine abstraite de Krivine (KAM), la construction des modèles, la réalisation de l'arithmétique et les deux principales problématiques calculatoires : la spécification et l'extraction de témoin. Pour illustrer la flexibilité de ce cadre, nous montrons ensuite qu'il s'adapte sans effort à diverses extensions : l'ajout d'instructions supplémentaires dans la KAM ou l'introduction de types de données primitifs tels que les entiers, les rationnels et les réels. Ces divers travaux ont été formalisés dans l'assistant de preuves Coq.Dans une seconde partie, nous redéfinissons ce cadre à l'ordre supérieur et le comparons à PA2. Ce changement, nécessaire pour exprimer pleinement la transformation de forcing, uniformise la théorie et permet d'intégrer tous les types de données. Nous présentons ensuite le forcing en réalisabilité classique, initialement dû à Krivine, puis l'étendons aux filtres génériques, lorsque les conditions de forcing forment un type de données. Cela permet de relire le forcing comme une transformation de programmes, dans le but d'obtenir des réalisateurs plus efficaces plutôt que des résultats d'indépendance. Cette méthode est illustrée notamment par l'exemple du théorème de Herbrand, dont la preuve par forcing donne un programme nettement plus efficace que la preuve habituelle. / This thesis focuses on the computational interpretation of Cohen's forcing through the classical Curry-Howard correspondence, using the tools of classical realizability. In a first part, we start by a general introduction to classical realizability in second-order arithmetic (PA2). We cover the description of the Krivine Abstract Machine (KAM), the construction of the realizability models, the realizers for arithmetic and the main two computational topics: specification and witness extraction. To illustrate the flexibility of this approach, we show that it can be effortlessly adapted to several extensions such as new instructions in the KAM or primitive datatypes like natural, rational and real numbers. These various works are formalized in the Coq proof assistant.In the second part, we redesign this framework in a higher-order setting and compare it to PA2.This change is necessary to fully express the forcing transformation, but it also allows us to uniformize the theory and integrate all datatypes. We present forcing in classical realizability, initially due to Krivine, and extend it to generic filters whenever the forcing conditions form a datatype. We can then see forcing as a program transformation adding a memory cell with its access primitives. Our aim is to find more efficient realizers rather than independence results, which are the common use of forcing techniques. The methodology is illustrated on the example of Herbrand's theorem, the proof by forcing of which gives a much more efficient program than the usual proof. Furthermore, we can recover the natural algorithm that one can write to solve the underlying computational problem if we use a datatype as forcing poset.

Étant donnée une fonction bornée (supérieurement ou inférieurement) $f:\mathbb{N}^k \To \Real$ par une expression mathématique, le problème de trouver les points extrémaux de $f$ sur chaque ensemble fini $S \subset \mathbb{N}^k$ est bien défini du point de vu classique. Du point de vue de la théorie de la calculabilité néanmoins il faut éviter les cas pathologiques où ce problème a une complexité de Kolmogorov infinie. La principale restriction consiste à définir l'ordre, parce que la comparaison entre les nombres réels n'est pas décidable. On résout ce problème grâce à une structure qui contient deux algorithmes, un algorithme d'analyse réelle récursive pour évaluer la fonction-coût en arithmétique à précision infinie et un autre algorithme qui transforme chaque valeur de cette fonction en un vecteur d'un espace, qui en général est de dimension infinie. On développe trois cas particuliers de cette structure, un de eux correspondant à la méthode d'approximation de Rauzy. Finalement, on établit une comparaison entre les meilleures approximations diophantiennes simultanées obtenues par la méthode de Rauzy (selon l'interprétation donnée ici) et une autre méthode, appelée tétraédrique, que l'on introduit à partir de l'espace vectoriel engendré par les logarithmes de nombres premiers. / Given a (lower or upper) bounded function $f:\mathbb{N}^k \To \Real$ by a mathematical expression. The problem to find the extremal points of $f$ on any bounded set $S \subset \mathbb{N}^k$ is well-defined from a classical point of view. Nevertheless, from a computability theory perspective, it should be avoided the possibility of pathologies when this problem has infinite Kolmogorov complexity. The main constraint is that the order relationship between computable reals is not effectively solvable. We solve this problem by means of a structure containing two algorithms. The first one allows to evaluate the cost function while the second one transforms each value of the cost function in a point in an infinite dimensional vector of a space. We develop three particular cases, one of them corresponding to the Rauzy approximation method. Finally, we make a comparison between the best simultaneous Diophantine approximations obtained by the Rauzy method (our optimization-oriented version of it) and our tetrahedral method, that is one of the main achievement of this work.

Cette thèse présente une formalisation des nombres algébriques et de leur théorie. Elle apporte deux nouvelles contributions importantes à la formalisation de résultats mathématiques dans des assistants à la preuve, ici Coq : la construction intuitionniste des nombres algébriques réels et la preuve qu'ils constituent un corps réel clos, ainsi que la programmation et la certification de procédures d'élimination des quantificateurs pour les théories des corps algébriquement clos et des corps réels clos. Pour atteindre ces résultats, nous avons apporté des contributions aux outils et aux méthodologies de preuves et de formalisation des mathématiques en Coq. En particulier, nous fournissons pour Coq/SSReflect un cadre pour travailler avec des types quotients. Nous fournissons une bibliothèque complète sur les structures algébriques de nombres ordonnés et normés. Nous avons réalisé une courte implémentation des réels de Cauchy accompagnée de tactiques pour effectuer facilement des raisonnements comportant des affirmations de la forme "soit n un entier suffisamment grand", couramment utilisés dans les preuves mathématiques sur papier. Nous avons également développé une petite bibliothèque d'analyse de base sur les polynômes à coefficients dans un corps réel clos. Une grande partie de nos résultats s'intègrent dans la formalisation de la preuve du théorème de Feit-Thompson et ont aussi pour objectif d'aider à certifier des procédures plus efficace d'élimination des quantificateurs sur les réels.

Cette recherche étudie l'enseignement des premiers éléments de l'Analyse réelle à la transition lycée/université à travers un modèle de variables macro-didactiques (VMD) relatives aux niveaux de formalisation et de familiarité des savoirs mathématiques proposés aux élèves. Lorsque l'on passe du lycée à l'université, les valeurs de ces variables sont dichotomiques et témoignent d'une profonde mutation dans le travail mathématique demandé. Nous nous posons la question des moyens que peut se donner l'enseignement des mathématiques, à l'entrée à l'université, pour gérer des variations aussi importantes et permettre aux étudiants d'accéder aux objets de l'Analyse réelle. <br />Une ingénierie a porté sur la construction et l'expérimentation, dans le cadre de la TSD (Théorie des Situations Didactiques), de deux situations sur les limites, que nous avons expérimentées à un niveau du cursus où seule l'existence formelle des objets de l'Analyse réelle a été établie par les professeurs. Nous avons ciblé le travail des étudiants sur les méthodes d'approximation, afin de favoriser des allers/retours entre les "preuves pragmatiques" géométriques ou numériques et l'utilisation des théorèmes d'Analyse. Les situations prennent en compte la dialectique sémantique/ syntaxique dans un processus de preuve, et permettent un retour efficace sur les savoirs visés. L'entrée dans un processus de preuves mixtes – pragmatiques vs formelles – a ainsi été rendu obligatoire dans le travail des étudiants, à travers l'émergence du problème général de l'existence et de l'accessibilité des nombres, des limites et des suites. <br />En conclusion, nous proposons de poursuivre l'étude du milieu théorique des situations de l'Analyse réelle, d'introduire d'autres situations expérimentales et d'étudier plus en profondeur les connaissances des étudiants dans le contrat didactique instauré par de telles situations.