Deligne and Howe described polarized abelian varieties over finite fields in terms of finitely generated free Z-modules satisfying a list of easy to state axioms. In this thesis we address the problem of developing an effective algorithm to compute isomorphism classes of (principally) polarized abelian varieties over a finite field, together with their automorphism groups. Performing such computations requires the knowledge of the ideal classes (both invertible and non-invertible) of certain orders in number fields. Hence we describe a method to compute the ideal class monoid of an order and we produce concrete computations in dimension 2, 3 and 4.

Let Ω be the Fraïssé limit of a class of relational structures. We seek to answer the following semigroup theoretic question about Ω. What are the group H-classes, i.e. the maximal subgroups, of End(Ω)? Fraïssé limits for which we answer this question include the random graph R, the random directed graph D, the random tournament T, the random bipartite graph B, Henson's graphs G[subscript n] (for n greater or equal to 3) and the total order Q. The maximal subgroups of End(Ω) are closely connected to the automorphism groups of the relational structures induced by the images of idempotents from End(Ω). It has been shown that the relational structure induced by the image of an idempotent from End(Ω) is algebraically closed. Accordingly, we investigate which groups can be realised as the automorphism group of an algebraically closed relational structure in order to determine the maximal subgroups of End(Ω) in each case. In particular, we show that if Γ is a countable graph and Ω = R,D,B, then there exist 2[superscript aleph-naught] maximal subgroups of End(Ω) which are isomorphic to Aut(Γ). Additionally, we provide a complete description of the subsets of Q which are the image of an idempotent from End(Q). We call these subsets retracts of Q and show that if Ω is a total order and f is an embedding of Ω into Q such that im f is a retract of Q, then there exist 2[superscript aleph-naught] maximal subgroups of End(Q) isomorphic to Aut(Ω). We also show that any countable maximal subgroup of End(Q) must be isomorphic to Zⁿ for some natural number n. As a consequence of the methods developed, we are also able to show that when Ω = R,D,B,Q there exist 2[superscript aleph-naught] regular D-classes of End(Ω) and when Ω = R,D,B there exist 2[superscript aleph-naught] J-classes of End(Ω). Additionally we show that if Ω = R,D then all regular D-classes contain 2[superscript aleph-naught] group H-classes. On the other hand, we show that when Ω = B,Q there exist regular D-classes which contain countably many group H-classes.

Peaks andThe main subject of this thesis is diagram rewriting.This is a generalisation to dimension~$2$ of word rewriting (in dimension~$1$). In a first time, we give the first convergent diagrammatic presentation of the PRO of linear maps in arbitrary field. Then we study the convergent diagrammatic presentation of matrix of isometries of $RR^n$. We focus especially on a rule similar to the Yang-Baxter equation, described by a certain map $h$. We use the confluence of critical the parametric diagrams, To study the algebraic properties of $h$, Finally, we present the $Sigma$-diagrams, an alternative approach for calculation in bialgebras. We illustrate this approach with examples. The last two chapters have been already published: Diagram rewriting for orthogonal matrices: a study of critical peaks, avec Yves Lafont, Lecture Notes in Computer Science 5117, p. 232-245, 2008 Properties of co-operations: diagrammatic proofs, Mathematical Structures in Computer Science 22(6), p. 970-986, 2012. / The main subject of this thesis is diagram rewriting.This is a generalisation to dimension~$2$ of word rewriting (in dimension~$1$). In a first time, we give the first convergent diagrammatic presentation of the PRO of linear maps in arbitrary field. Then we study the convergent diagrammatic presentation of matrix of isometries of $RR^n$. We focus especially on a rule similar to the Yang-Baxter equation, described by a certain map $h$. We use the confluence of criticalthe parametric diagrams, To study the algebraic properties of $h$, Finally, we present the $Sigma$-diagrams, an alternative approach for calculation in bialgebras. We illustrate this approach with examples. The last two chapters have been already published: Diagram rewriting for orthogonal matrices: a study of critical peaks, avec Yves Lafont, Lecture Notes in Computer Science 5117, p. 232-245, 2008 Properties of co-operations: diagrammatic proofs, Mathematical Structures in Computer Science 22(6), p. 970-986, 2012.

Cette thèse se situe au carrefour de la combinatoire énumérative, algébrique et bijective. Elle se consacre d’une part à traduire des problèmes algébriques en des problèmes combinatoires, et inversement, utilise le formalisme algébrique pour traiter des questions combinatoires.Après un rappel des notions classiques de combinatoire et de structures algébriques, nous abordons l’étude des tableaux de dominos décalés, qui sont des objets combinatoires définis dans le but de mieux comprendre la combinatoire des fonctions symétriques P et Q de Schur. Nous donnons la définition de ces tableaux et nous démontrons qu'ils sont en bijection avec les paires de tableaux de Young décalés. Cette bijection nous permet de voir ces objets comme des éléments du super monoïde plaxique décalé, qui est l'analogue décalé du super monoïde plaxique de Carré et Leclerc. Nous montrons aussi que ces tableaux décrivent un produit de deux fonctions P de Schur et en prenant un autre type de tableaux de dominos décalés, nous décrivons un produit de deux fonctions Q de Schur. Nous proposons aussi deux algorithmes d'insertion pour les tableaux de dominos décalés, analogues aux algorithmes d'insertion mixte et d'insertion gauche-droit de Haiman. Toujours dans le domaine de la combinatoire bijective, nous nous intéressons dans la deuxième partie de notre travail à des bijections en lien avec des statistiques sur les permutations et les nombres eulériens.Dans cette deuxième partie de thèse, nous introduisons l'unimodalité des suites finies associées aux différentes directions dans le triangle eulérien. Nous donnons dans un premier temps une interprétation combinatoire ainsi que la relation de récurrence des suites associées à la direction (1,t) dans le triangle eulérien, où t≥1. Ces suites sont les coefficients de polynômes appelés les polynômes eulériens avec succession d'ordre t, qui généralisent les polynômes eulériens. Nous démontrons par une bijection entre les permutations et des chemins nord-est étiquetés que ces suites sont log-concaves et donc unimodales. Puis nous prouvons que les suites associées aux directions (r,q), où r est un entier positif et q est un entier, tel que r+q≥0, sont aussi log-concaves et donc unimodales / This thesis is at the crossroads of enumerative, algebraic and bijective combinatorics. It studies some algebraic problems from a combinatorial point of view, and conversely, uses algebraic formalism to deal with combinatorial questions.After a reminder about classical notions of combinatoics and algebraic structures, We introduce new combinatorial objects called the shifted domino tableaux, these objects can be seen as a shifted analog of domino tableaux or as an extension of shifted Young tableaux. We prove that these objects are in bijection with pairs of shifted Young tableaux. This bijection shows that shifted domino tableaux can be seen as elements of the super shifted plactic monoid, which is the shifted analog of the super plactic monoid. We also show that the sum over all shifted domino tableaux of a fixed shape describe a product of two P-Schur functions, and by taking a different kind of shifted domino tableaux we describe a product of two Q-Schur functions. We also propose two insertion algorithms for shifted domino tablaux, analogous to Haiman's left-right and mixed insertion algorithms. Still in the field of bijective combinatorics, we are interested in the second part of our work with bijections related to statistics on permutations and Eulerian numbers.In this second part of this thesis, we introduce the unimodality of finite sequences associated to different directions in the Eulerian triangle. We first give a combinatorial interpretations as well as recurrence relations of sequences associated with the direction (1, t) in the Eulerian triangle, where t≥1. These sequences are the coefficients of polynomials called the t-successive eulerian polynomials, which generalize the eulerian polynomials. We prove using a bijection between premutations and north-east lattice paths that those sequences are unomodal. Then we prove that the sequences associated with the directions (r, q), where r is a positive integer and q is an integer such that r + q ≥ 0, are also log-concave and therefore unimodal

Dependent type theories are a kind of mathematical foundations investigated both for the formalisation of mathematics and for reasoning about programs. They are implemented as the kernel of many proof assistants and programming languages with proofs (Coq, Agda, Idris, Dedukti, Matita, etc). Dependent types allow to encode elegantly and constructively the universal and existential quantifications of higher-order logics and are therefore adapted for writing logical propositions and proofs. However, their usage is not limited to the area of pure logic. Indeed, some recent work has shown that they can also be powerful for driving the construction of programs. Using more precise types not only helps to gain confidence about the program built, but it can also help its construction, giving rise to a new style of programming called Type-Driven Development. However, one difficulty with reasoning and programming with dependent types is that proof obligations arise naturally once programs become even moderately sized. For example, implementing an adder for binary numbers indexed over their natural number equivalents naturally leads to proof obligations for equalities of expressions over natural numbers. The need for these equality proofs comes, in intensional type theories (like CIC and ML) from the fact that in a non-empty context, the propositional equality allows us to prove as equal (with the induction principles) terms that are not judgementally equal, which implies that the typechecker can't always obtain equality proofs by reduction. As far as possible, we would like to solve such proof obligations automatically, and we absolutely need it if we want dependent types to be use more broadly, and perhaps one day to become the standard in functional programming. In this thesis, we show one way to automate these proofs by reflection in the dependently typed programming language Idris. However, the method that we follow is independent from the language being used, and this work could be reproduced in any dependently-typed language. We present an original type-safe reflection mechanism, where reflected terms are indexed by the original Idris expression that they represent, and show how it allows us to easily construct and manipulate proofs. We build a hierarchy of correct-by-construction tactics for proving equivalences in semi-groups, monoids, commutative monoids, groups, commutative groups, semi-rings and rings. We also show how each tactic reuses those from simpler structures, thus avoiding duplication of code and proofs. Finally, and as a conclusion, we discuss the trust we can have in such machine-checked proofs.

Cette thèse développe des algorithmes pour les problèmes de plus court chemin sous cont-rain-tes de ressources, et les applique à l'optimisation des rotations des avions et des équipages d'une compagnie aérienne dans le cadre d'approches par génération de colonnes.Les problèmes de plus court chemin sous contraintes de ressources sont généralement résolus grâce à une énumération intelligente de tous les chemins non dominés. Les approches récentes utilisent des bornes sur les ressources des chemins pour éliminer des solutions partielles. L'efficacité de la méthode est conditionnée par la qualité des bornes utilisées. Notre principale contribution au domaine est l'introduction d'une procédure générique pour calculer des bornes qui s'applique à la plupart des problèmes de chemins sous contraintes, et en particulier les problèmes stochastiques. A cette fin, nous introduisons une généralisation du problème de plus court chemin sous contraintes dans laquelle les ressources des chemins appartiennent à un monoïde ordonné comme un treillis. La ressource d'un chemin est la somme des ressources de ses arcs, le terme somme désignant l'opérateur du monoïde. Le problème consiste à trouver parmi les chemins qui satisfont une contrainte donnée celui dont la ressource minimise une fonction de coût croissante de la ressource des chemins. Nous généralisons les algorithmes d'énumération à ce nouveau problème. La théorie des treillis nous permet de construire une procédure polynomiale pour trouver des bornes de qualité. L'efficacité pratique de la méthode est évaluée au travers d'une étude numérique détaillée sur des problèmes de chemins déterministes et stochastiques. Les procédures de calcul des bornes peuvent être interprétées comme des généralisations aux monoïdes ordonnés comme des treillis d'algorithmes de la littérature définis pour résoudre un problème de chemin pour lequel les ressources des chemins prennent leur valeur dans un semi-anneau.Nos algorithmes de chemins ont été appliqués avec succès au problème de crew pairing. Étant donné un ensemble de vols opérés par une compagnie aérienne, les problèmes d'aircraft routing et de crew pairing construisent respectivement les séquences de vols opérées par les avions et par les équipages de manière à couvrir tous les vols à moindre coût. Comme certaines séquences de vols ne peuvent être réalisées par un équipage que s'il reste dans le même avion, les deux problèmes sont liés. La pratique actuelle dans l'industrie aéronautique est de résoudre tout d'abord le problème d'aircraft routing, puis le problème de crew pairing, ce qui aboutit à une solution non-optimale. Des méthodes de résolution pour le problème intégré ont été développées ces dix dernières années. Nous proposons une méthode de résolution pour le problème intégré reposant sur deux nouveaux ingrédients : un programme linéaire en nombre entier compact pour le problème d'aircraft routing, ainsi que de nouveaux pour le problème esclave de l'approche usuelle par génération de colonnes du problème de crew pairing. Ces algorithmes pour le problème esclave sont une application de nos algorithmes pour le problème de plus court chemin sous contraintes. Nous généralisons ensuite cette approche de manière à prendre en compte des contraintes de probabilités sur la propagation du retard. Ces algorithmes permettent de résoudre quasiment à l'optimum les instances industrielles d'Air France / This thesis develops algorithms for resource constrained shortest path problems, and uses them to solve the pricing subproblems of column generation approaches to some airline operations problems.Resource constrained shortest path problems are usually solved using a smart enumeration of the non-dominated paths. Recent improvements of these enumeration algorithms rely on the use of bounds on path resources to discard partial solutions. The quality of the bounds determines the performance of the algorithm. Our main contribution to the topic is to introduce a standard procedure to generate bounds on paths resources in a general setting which covers most resource constrained shortest path problems, among which stochastic versions. In that purpose, we introduce a generalization of the resource constrained shortest path problem where the resources are taken in a lattice ordered monoid. The resource of a path is the monoid sum of the resources of its arcs. The problem consists in finding a path whose resource minimizes a non-decreasing cost function of the path resource among the paths that satisfy a given constraint. Enumeration algorithms are generalized to this framework. We use lattice theory to provide polynomial procedures to find good quality bounds. The efficiency of the approach is proved through an extensive numerical study on deterministic and stochastic path problems. Interestingly, the bounding procedures can be seen as generalizations to lattice ordered monoids of some algebraic path problem algorithms which initially work with resources in a semiring.Given a set of flight legs operated by an airline, the aircraft routing and the crew pairing problem build respectively the sequences of flight legs operated by airplanes and crews at minimum cost. As some sequences of flight legs can be operated by crews only if they stay in the same aircraft, the two problems are linked. The current practice in the industry is to solve first the aircraft routing, and then the crew pairing problem, leading to a non-optimal solution. During the last decade, solution schemes for the integrated problem have been developed. We propose a solution scheme for the integrated problem based on two new ingredients: a compact integer program approach to the aircraft routing problem, and a new algorithm for the pricing subproblem of the usual column generation approach to the crew pairing problem, which is based on our resource constrained shortest path framework. We then generalize the algorithm to take into account delay propagation through probabilistic constraints. The algorithms enable to solve to near optimality Air France industrial instances