Nous adaptons une heuristique de recherche à voisinage variable pour traiter le problème du voyageur de commerce avec fenêtres de temps (TSPTW) lorsque l'objectif est la minimisation du temps d'arrivée au dépôt de destination. Nous utilisons des méthodes efficientes pour la vérification de la réalisabilité et de la rentabilité d'un mouvement. Nous explorons les voisinages dans des ordres permettant de réduire l'espace de recherche. La méthode résultante est compétitive avec l'état de l'art. Nous améliorons les meilleures solutions connues pour deux classes d'instances et nous fournissons les résultats de plusieurs instances du TSPTW pour la première fois. / We adapt a general variable neighborhood search heuristic to solve the traveling salesman problem with time windows (TSPTW) where the objective is to minimize the completion time. We use efficient methods to check the feasibility and the profitability of a movement. We use a specific order to reduce the search space while exploring the neighborhoods. The resulting method is competitive with the state-of-the-art. We improve the best known solutions for two classes of instances and provide the results of multiple instances of TSPTW for the first time.

Dans cette thèse, nous nous étudions des algorithmes d’optimisation non linéaire. D’une part nous proposons des techniques de détection rapide de la non-réalisabilité d’un problème à résoudre. D’autre part, nous analysons le comportement local des algorithmes pour la résolution de problèmes singuliers. Dans la première partie, nous présentons une modification d’un algorithme de lagrangien augmenté pour l’optimisation avec contraintes d’égalité. La convergence quadratique du nouvel algorithme dans le cas non-réalisable est démontrée théoriquement et numériquement. La seconde partie est dédiée à l’extension du résultat précédent aux problèmes d’optimisation non linéaire généraux avec contraintes d’égalité et d’inégalité. Nous proposons une modification d’un algorithme de pénalisation mixte basé sur un lagrangien augmenté et une barrière logarithmique. Les résultats théoriques de l’analyse de convergence et quelques tests numériques montrent l’avantage du nouvel algorithme dans la détection de la non-réalisabilité. La troisième partie est consacrée à étudier le comportement local d’un algorithme primal-dual de points intérieurs pour l’optimisation sous contraintes de borne. L’analyse locale est effectuée sans l’hypothèse classique des conditions suffisantes d’optimalité de second ordre. Celle-ci est remplacée par une hypothèse plus faible basée sur la notion de borne d’erreur locale. Nous proposons une technique de régularisation de la jacobienne du système d’optimalité à résoudre. Nous démontrons ensuite des propriétés de bornitude de l’inverse de ces matrices régularisées, ce qui nous permet de montrer la convergence superlinéaire de l’algorithme. La dernière partie est consacrée à l’analyse de convergence locale de l’algorithme primal-dual qui est utilisé dans les deux premières parties de la thèse. En pratique, il a été observé que cet algorithme converge rapidement même dans le cas où les contraintes ne vérifient l’hypothèse de qualification de Mangasarian-Fromovitz. Nous démontrons la convergence superlinéaire et quadratique de cet algorithme, sans hypothèse de qualification des contraintes. / This thesis is devoted to the study of numerical algorithms for nonlinear optimization. On the one hand, we propose new strategies for the rapid infeasibility detection. On the other hand, we analyze the local behavior of primal-dual algorithms for the solution of singular problems. In the first part, we present a modification of an augmented Lagrangian algorithm for equality constrained optimization. The quadratic convergence of the new algorithm in the infeasible case is theoretically and numerically demonstrated. The second part is dedicated to extending the previous result to the solution of general nonlinear optimization problems with equality and inequality constraints. We propose a modification of a mixed logarithmic barrier-augmented Lagrangian algorithm. The theoretical convergence results and the numerical experiments show the advantage of the new algorithm for the infeasibility detection. In the third part, we study the local behavior of a primal-dual interior point algorithm for bound constrained optimization. The local analysis is done without the standard assumption of the second-order sufficient optimality conditions. These conditions are replaced by a weaker assumption based on a local error bound condition. We propose a regularization technique of the Jacobian matrix of the optimality system. We then demonstrate some boundedness properties of the inverse of these regularized matrices, which allow us to prove the superlinear convergence of our algorithm. The last part is devoted to the local convergence analysis of the primal-dual algorithm used in the first two parts of this thesis. In practice, it has been observed that this algorithm converges rapidly even in the case where the constraints do not satisfy the Mangasarian-Fromovitz constraint qualification. We demonstrate the superlinear and quadratic convergence of this algorithm without any assumption of constraint qualification.

Cette thèse porte sur l’adaptation de la réalisabilité et la paramétricité au cas des types dépendants dans le cadre des Systèmes de Types Purs. Nous décrivons une méthode systématique pour construire une logique à partir d’un langage de programmation, tous deux décrits comme des systèmes de types purs. Cette logique fournit des formules pour exprimer des propriétés des programmes et elle offre un cadre formel adéquat pour développer une théorie de la réalisabilité au sein de laquelle les réalisateurs des formules sont exactement les programmes du langage de départ. Notre cadre permet alors de considérer les théorèmes de représentation pour le système T de Gödel et le système F de Girard comme deux instances d'un théorème plus général.Puis, nous expliquons comment les relations logiques de la théorie de la paramétricité peuvent s'exprimer en terme de réalisabilité, ce qui montre que la logique engendrée fournit un cadre adéquat pour développer une théorie de la paramétricité du langage de départ. Pour finir, nous montrons comment cette théorie de la paramétricité peut-être adaptée au système sous-jacent à l'assistant de preuve Coq et nous donnons un exemple d'application original de la paramétricité à la formalisation des mathématiques. / This thesis focuses on the adaptation of realizability and parametricity to dependent types in the framework of Pure Type Systems. We describe a systematic method to build a logic from a programming language, both described as pure type systems. This logic provides formulas to express properties of programs and offers a formal framework that allows us to develop a theory of realizability in which realizers of formulas are exactly programs of the starting programming language. In our framework, the standard representation theorems of Gödel's system T and Girard's system F may be seen as two instances of a more general theorem. Then, we explain how the so-called « logical relations » of parametricity theory may be expressed in terms of realizability, which shows that the generated logic provides an adequate framework for developping a general theory of parametricity. Finally, we show how this parametricity theory can be adapted to the underlying type system of the proof assistant Coq and we give an original example of application of parametricity theory to the formalization of mathematics.