Ce mémoire comporte deux parties distinctes. La première partie concerne une étude d'algèbres n-aires. Une algèbre n-aire est un espace vectoriel sur lequel est définie une multiplication sur n arguments. Classiquement les multiplications sont binaires, mais depuis l'utilisation en physique théorique de multiplications ternaires, comme les produits de Nambu, de nombreux travaux mathématiques se sont focalisés sur ce type d'algèbres. Deux classes d'algèbres n-aires sont essentielles: les algèbres n-aires associatives et les algèbres n-aires de Lie. Nous nous intéressons aux deux classes. Concernant les algèbres n-aires associatives, on s'intéresse surtout aux algèbres 3-aires partiellement associatives, c'est-à-dire dont la multiplication vérifie l'identité ((xyz)tu)+(x(yzt)u)+(xy(ztu))=0 Ce cas est intéressant car les travaux connus concernant ce type d'algèbres ne distinguent pas les cas n pair et n-impair. On montre dans cette thèse que le cas n=3 ne peut pas être traité comme si n était pair. On étudie en détail l'algèbre libre 3-aire partiellement associative sur un espace vectoriel de dimension finie. Cette algèbre est graduée et on calcule précisément les dimensions des 7 premières composantes. On donne dans le cas général un système de générateurs ayant la propriété qu'une base est donnée par la sous famille des éléments non nuls. Les principales conséquences sont L'algèbre libre 3-aire partiellement associative est résoluble. L'algèbre libre commutative 3-aire partiellement associative est telle que tout produit concernant 9 éléments est nul. L'opérade quadratique correspondant aux algèbres 3-aires partiellement associatives ne vérifient pas la propriété de Koszul. On s'intéresse ensuite à l'étude des produits n-aires sur les tenseurs. L'exemple le plus simple est celui d'un produit interne sur des matrices non carrées. Nous pouvons définir le produit 3aire donné par A . ^tB . C. On montre qu'il est nécessaire de généraliser un peu la définition de partielle associativité. Nous introduisons donc les produits -partiellement associatifs où  est une permutation de degré p. Concernant les algèbres de Lie n-aires, deux classes d'algèbres ont été définies: les algèbres de Fillipov (aussi appelées depuis peu les algèbres de Lie-Nambu) et les algèbres n-Lie. Cette dernière notion est très générale. Cette dernière notion, très important dans l'étude de la mécanique de Nambu-Poisson, est un cas particulier de la première. Mais pour définir une approche du type Maurer-Cartan, c'est-à-dire définir une cohomologie scalaire, nous considérons dans ce travail les algèbres de Fillipov comme des algèbres n-Lie et développons un tel calcul dans le cadre des algèbres n-Lie. On s'intéresse également à la classification des algèbres n-aires nilpotentes. Le dernier chapitre de cette partie est un peu à part et reflète un travail poursuivant mon mémoire de Master. Il concerne les algèbres de Poisson sur l'algèbre des polynômes. On commence à présenter le crochet de Poisson sous forme duale en utilisant des équations de Pfaff. On utilise cette approche pour classer les structures de Poisson non homogènes sur l’algèbre des polynômes à trois variables . Le lien avec les algèbres de Lie est clair. Du coup on étend notre étude aux algèbres de Poisson dont l'algèbre de Lie sous jacent est rigide et on applique les résultats aux algèbres enveloppantes des algèbres de Lie rigides. La partie 2 concerne l'arithmétique des intervalles. Cette étude a été faite suite à une rencontre avec une société d'ingénierie travaillant sur des problèmes de contrôle de paramètres, de problème inverse (dans quels domaines doivent évoluer les paramètres d'un robot pour que le robot ait un comportement défini). [...] / This thesis has two distinguish parts. The first part concerns the study of n-ary algebras. A n-ary algebra is a vector space with a multiplication on n arguments. Classically the multiplications are binary, but the use of ternary multiplication in theoretical physic like for Nambu brackets led mathematicians to investigate these type of algebras. Two classes of n-ary algebras are fundamental: the associative n-ary algebras and the Lie n-ary algebras. We are interested by both classes. Concerning the associative n-ary algebras we are mostly interested in 3-ary partially associative 3-ary algebras, that is, algebras whose multiplication satisfies ((xyz)tu)+(x(yzt)u)+(xy(ztu))=0. This type is interesting because the previous woks on this subject was not distinguish the even and odd cases. We show in this thesis that the case n=3 can not be treated as the even cases. We investigate in detail the free partially associative 3-ary algebra on k generators. This algebra is graded and we compute the dimensions of the 7 first components. In the general case, we give a spanning set such as the sub family of non zero vector is a basis. The main consequences are the free partially associative 3-ary algebra is solvable. In the free commutative partially associative 3-ary algebra any product on 9 elements is trivial. The operad for partially associative 3-ary algebra do not satisfy the Koszul property. Then we study n-ary products on the tensors. The simplest example is given by a internal product of non square matrices. We can define a 3-ary product by taking A . ^tB . C. We show that we have to generalize a bit the definition of partial associativity for n-ary algebras. We then introduce the products -partially associative where  is a permutation of the symmetric group of degree n. Concerning the n-ary algebras, two classes have been defined: Filipov algebras (also called recently Lie-Nambu algebras) and some more general class, the n-Lie algebras. Filipov algebras are very important in the study of the mechanic of Nambu-Poisson, and is a particular case of the other. So to define an approach of Maurer-Cartan type, that is, define a scalar cohomology, we consider in this work Fillipov as n-Lie algebras and develop such a calculus in the n-Lie algebras frame work. We also give some classifications of n-ary nilpotent algebras. The last chapter of this part concerns my work in Master on the Poisson algebras on polynomials. We present link with the Lie algebras is clear. Thus we extend our study to Poisson algebras which associated Lie algebra is rigid and we apply these results to the enveloping algebras of rigid Lie algebras. The second part concerns intervals arithmetic. The interval arithmetic is used in a lot of problems concerning robotic, localization of parameters, and sensibility of inputs. The classical operations of intervals are based of the rule : the result of an operation of interval is the minimal interval containing all the result of this operation on the real elements of the concerned intervals. But these operations imply many problems because the product is not distributive with respect the addition. In particular it is very difficult to translate in the set of intervals an algebraic functions of a real variable. We propose here an original model based on an embedding of the set of intervals on an associative algebra. Working in this algebra, it is easy to see that the problem of non distributivity disappears, and the problem of transferring real function in the set of intervals becomes natural. As application, we study matrices of intervals and we solve the problem of reduction of intervals matrices (diagonalization, eigenvalues, and eigenvectors).

Les surfaces de subdivision fournissent une méthode alternative prometteuse dans la modélisation géométrique, et ont des avantages sur la représentation classique de trimmed-NURBS, en particulier dans la modélisation de surfaces lisses par morceaux. Dans ce mémoire, nous considérons le problème des opérations géométriques sur les surfaces de subdivision, avec l'exigence stricte de forme topologique correcte. Puisque ce problème peut être mal conditionné, nous proposons une approche pour la gestion de l'incertitude qui existe dans le calcul géométrique. Nous exigeons l'exactitude des informations topologiques lorsque l'on considère la nature de robustesse du problème des opérations géométriques sur les modèles de solides, et il devient clair que le problème peut être mal conditionné en présence de l'incertitude qui est omniprésente dans les données. Nous proposons donc une approche interactive de gestion de l'incertitude des opérations géométriques, dans le cadre d'un calcul basé sur la norme IEEE arithmétique et la modélisation en surfaces de subdivision. Un algorithme pour le problème planar-cut est alors présenté qui a comme but de satisfaire à l'exigence topologique mentionnée ci-dessus. / Subdivision surfaces are a promising alternative method for geometric modelling, and have some important advantages over the classical representation of trimmed-NURBS, especially in modelling piecewise smooth surfaces. In this thesis, we consider the problem of geometric operations on subdivision surfaces with the strict requirement of correct topological form, and since this problem may be ill-conditioned, we propose an approach for managing uncertainty that exists inherently in geometric computation. We take into account the requirement of the correctness of topological information when considering the nature of robustness for the problem of geometric operations on solid models, and it becomes clear that the problem may be ill-conditioned in the presence of uncertainty that is ubiquitous in the data. Starting from this point, we propose an interactive approach of managing uncertainty of geometric operations, in the context of computation using the standard IEEE arithmetic and modelling using a subdivision-surface representation. An algorithm for the planar-cut problem is then presented, which has as its goal the satisfaction of the topological requirement mentioned above.

Les surfaces de subdivision fournissent une méthode alternative prometteuse dans la modélisation géométrique, et ont des avantages sur la représentation classique de trimmed-NURBS, en particulier dans la modélisation de surfaces lisses par morceaux. Dans ce mémoire, nous considérons le problème des opérations géométriques sur les surfaces de subdivision, avec l'exigence stricte de forme topologique correcte. Puisque ce problème peut être mal conditionné, nous proposons une approche pour la gestion de l'incertitude qui existe dans le calcul géométrique. Nous exigeons l'exactitude des informations topologiques lorsque l'on considère la nature de robustesse du problème des opérations géométriques sur les modèles de solides, et il devient clair que le problème peut être mal conditionné en présence de l'incertitude qui est omniprésente dans les données. Nous proposons donc une approche interactive de gestion de l'incertitude des opérations géométriques, dans le cadre d'un calcul basé sur la norme IEEE arithmétique et la modélisation en surfaces de subdivision. Un algorithme pour le problème planar-cut est alors présenté qui a comme but de satisfaire à l'exigence topologique mentionnée ci-dessus. / Subdivision surfaces are a promising alternative method for geometric modelling, and have some important advantages over the classical representation of trimmed-NURBS, especially in modelling piecewise smooth surfaces. In this thesis, we consider the problem of geometric operations on subdivision surfaces with the strict requirement of correct topological form, and since this problem may be ill-conditioned, we propose an approach for managing uncertainty that exists inherently in geometric computation. We take into account the requirement of the correctness of topological information when considering the nature of robustness for the problem of geometric operations on solid models, and it becomes clear that the problem may be ill-conditioned in the presence of uncertainty that is ubiquitous in the data. Starting from this point, we propose an interactive approach of managing uncertainty of geometric operations, in the context of computation using the standard IEEE arithmetic and modelling using a subdivision-surface representation. An algorithm for the planar-cut problem is then presented, which has as its goal the satisfaction of the topological requirement mentioned above.

L'arithmétique par intervalles permet de calculer et simultanément vérifier des résultats. Cependant, une application naïve de cette arithmétique conduit à un encadrement grossier des résultats. De plus, de tels calculs peuvent être lents.Nous proposons des algorithmes précis et des implémentations efficaces, utilisant l'arithmétique par intervalles, dans le domaine de l'algèbre linéaire. Deux problèmes sont abordés : la multiplication de matrices à coefficients intervalles et la résolution vérifiée de systèmes linéaires. Pour le premier problème, nous proposons deux algorithmes qui offrent de bons compromis entre vitesse et précision. Pour le second problème, nos principales contributions sont d'une part une technique de relaxation, qui réduit substantiellement le temps d'exécution de l'algorithme, et d'autre part l'utilisation d'une précision étendue en quelques portions bien choisies de l'algorithme, afin d'obtenir rapidement une grande précision. / Interval arithmetic is a means to compute verified results. However, a naive use of interval arithmetic does not provide accurate enclosures of the exact results. Moreover, interval arithmetic computations can be time-consuming. We propose several accurate algorithms and efficient implementations in verified linear algebra using interval arithmetic. Two fundamental problems are addressed, namely the multiplication of interval matrices and the verification of a floating-point solution of a linear system. For the first problem, we propose two algorithms which offer new tradeoffs between speed and accuracy. For the second problem, which is the verification of the solution of a linear system, our main contributions are twofold. First, we introduce a relaxation technique, which reduces drastically the execution time of the algorithm. Second, we propose to use extended precision for few, well-chosen parts of the computations, to gain accuracy without losing much in term of execution time.

L'implantation en Virgule Flottante (VF) d'une fonction à valeurs réelles est réalisée avec arrondi correct si le résultat calculé est toujours égal à l'arrondi de la valeur exacte, ce qui présente de nombreux avantages. Mais pour implanter une fonction avec arrondi correct de manière fiable et efficace, il faut résoudre le "dilemme du fabricant de tables" (TMD en anglais). Deux algorithmes sophistiqués (L et SLZ) ont été conçus pour résoudre ce problème, via des calculs longs et complexes effectués par des implantations largement optimisées. D'où la motivation d'apporter des garanties fortes sur le résultat de ces pré-calculs coûteux. Dans ce but, nous utilisons l'assistant de preuves Coq. Tout d'abord nous développons une bibliothèque d'"approximation polynomiale rigoureuse", permettant de calculer un polynôme d'approximation et un intervalle bornant l'erreur d'approximation à l'intérieur de Coq. Cette formalisation est un élément clé pour valider la première étape de SLZ, ainsi que l'implantation d'une fonction mathématique en général (avec ou sans arrondi correct). Puis nous avons implanté en Coq, formellement prouvé et rendu effectif 3 vérifieurs de certificats, dont la preuve de correction dérive du lemme de Hensel que nous avons formalisé dans les cas univarié et bivarié. En particulier, notre "vérifieur ISValP" est un composant clé pour la certification formelle des résultats générés par SLZ. Ensuite, nous nous sommes intéressés à la preuve mathématique d'algorithmes VF en "précision augmentée" pour la racine carré et la norme euclidienne en 2D. Nous donnons des bornes inférieures fines sur la plus petite distance non nulle entre sqrt(x²+y²) et un midpoint, permettant de résoudre le TMD pour cette fonction bivariée. Enfin, lorsque différentes précisions VF sont disponibles, peut survenir le phénomène de "double-arrondi", qui peut changer le comportement de petits algorithmes usuels en arithmétique. Nous avons prouvé en Coq un ensemble de théorèmes décrivant le comportement de Fast2Sum avec double-arrondis.

L'implantation en Virgule Flottante (VF) d'une fonction à valeurs réelles est réalisée avec arrondi correct si le résultat calculé est toujours égal à l'arrondi de la valeur exacte, ce qui présente de nombreux avantages. Mais pour implanter une fonction avec arrondi correct de manière fiable et efficace, il faut résoudre le «dilemme du fabricant de tables» (TMD en anglais). Deux algorithmes sophistiqués (L et SLZ) ont été conçus pour résoudre ce problème, via des calculs longs et complexes effectués par des implantations largement optimisées. D'où la motivation d'apporter des garanties fortes sur le résultat de ces pré-calculs coûteux. Dans ce but, nous utilisons l'assistant de preuves Coq. Tout d'abord nous développons une bibliothèque d'«approximation polynomiale rigoureuse», permettant de calculer un polynôme d'approximation et un intervalle bornant l'erreur d'approximation à l'intérieur de Coq. Cette formalisation est un élément clé pour valider la première étape de SLZ, ainsi que l'implantation d'une fonction mathématique en général (avec ou sans arrondi correct). Puis nous avons implanté en Coq, formellement prouvé et rendu effectif 3 vérifieurs de certificats, dont la preuve de correction dérive du lemme de Hensel que nous avons formalisé dans les cas univarié et bivarié. En particulier, notre «vérifieur ISValP» est un composant clé pour la certification formelle des résultats générés par SLZ. Ensuite, nous nous sommes intéressés à la preuve mathématique d'algorithmes VF en «précision augmentée» pour la racine carré et la norme euclidienne en 2D. Nous donnons des bornes inférieures fines sur la plus petite distance non nulle entre sqrt(x²+y²) et un midpoint, permettant de résoudre le TMD pour cette fonction bivariée. Enfin, lorsque différentes précisions VF sont disponibles, peut survenir le phénomène de «double-arrondi», qui peut changer le comportement de petits algorithmes usuels en arithmétique. Nous avons prouvé en Coq un ensemble de théorèmes décrivant le comportement de Fast2Sum avec double-arrondis. / The Floating-Point (FP) implementation of a real-valued function is performed with correct rounding if the output is always equal to the rounding of the exact value, which has many advantages. But for implementing a function with correct rounding in a reliable and efficient manner, one has to solve the ``Table Maker's Dilemma'' (TMD). Two sophisticated algorithms (L and SLZ) have been designed to solve this problem, relying on some long and complex calculations that are performed by some heavily-optimized implementations. Hence the motivation to provide strong guarantees on these costly pre-computations. To this end, we use the Coq proof assistant. First, we develop a library of ``Rigorous Polynomial Approximation'', allowing one to compute an approximation polynomial and an interval that bounds the approximation error in Coq. This formalization is a key building block for verifying the first step of SLZ, as well as the implementation of a mathematical function in general (with or without correct rounding). Then we have implemented, formally verified and made effective 3 interrelated certificates checkers in Coq, whose correctness proof derives from Hensel's lemma that we have formalized for both univariate and bivariate cases. In particular, our ``ISValP verifier'' is a key component for formally verifying the results generated by SLZ. Then, we have focused on the mathematical proof of ``augmented-precision'' FP algorithms for the square root and the Euclidean 2D norm. We give some tight lower bounds on the minimum non-zero distance between sqrt(x²+y²) and a midpoint, allowing one to solve the TMD for this bivariate function. Finally, the ``double-rounding'' phenomenon can typically occur when several FP precision are available, and may change the behavior of some usual small FP algorithms. We have formally verified in Coq a set of results describing the behavior of the Fast2Sum algorithm with double-roundings.