On utilise la théorie de Floquet-Lin pour des systèmes différentiels linéaires quasi- périodiques pour établir des résultats d'existence et d'unicité et de dépendance continue des systèmes différentiels non linéaires quasi-périodiques. Et dans un second temps on établit un résultat de réductibilité d'un système différentiel linéaire presque-périodique en un système différentiel linéaire triangulaire supérieur avec conservation du nombre des solutions presque-périodiques indépendantes. Ensuite, un résultat d’existence et d’unicité et de dépendance continue des systèmes différentiels non linéaires presque-périodiques par rapport au terme du contrôle. / We use a Floquet theory for quasi-periodic linear ordinary differential equations due to Zhensheng Lin to obtain results, of existence, unicity, continuous and differentiable dependence, on the quasi-periodic solutions of quasi-periodic nonlinear ordinary differential equations. in a second time we establish the reducibility of linear systems of almost periodic differential equations into upper triangular systems of a. p. differential equations. This is done while the number of independent a. p. solutions is conserved. We prove existence and uniqueness of a. p. solutions of a nonlinear system with an a. p. linear part. Also we prove the continuous dependence of a. p. solutions of a nonlinear system with respect to an a. p. control term.

Dans ce document, nous montrons comment la notion de calculabilité introduite par W. W. Tait et étendue par Girard aux types polymorphes peut être utilisée et facilement étendue pour montrer la terminaison de différents types de relations de réécriture, y compris avec filtrage sur des symboles définis, filtrage d'ordre supérieur ou réécriture de classe modulo certaines théories équationnelles. Nous montrons également que la notion de clôture de calculabilité donne lieu a une relation bien fondée incluant l'extension à l'ordre supérieur par J.-P. Jouannaud et A. Rubio de l'ordre récursif sur les chemins de N. Dershowitz.

La notion de théorie s'est séparée de la notion de logique à la fin des années 1920, lorsque Hilbert et Ackermann ont distingué les règles de déduction, indépendantes de l'ob jet du discours, des axiomes qui lui sont spécifiques. S'est alors posée la question de caractériser les théories, définies donc comme des ensembles d'axiomes, que l'on peut utiliser pour formaliser une partie du raisonnement mathématique. Un premier critère est la cohérence de cette théorie : le fait qu'on ne puisse pas démontrer toutes les propositions de cette théorie. Cependant il est progressivement apparu que la cohérence n'était pas une propriété suffisante. Le fait que les démonstrations constructives vérifient les propriétés de la dijonction ou du témoin, ou la complétude de certaines méthodes de démonstration automatique ne découlent pas de la seule cohérence d'une théorie. Mais toutes trois sont par contre conséquentes d'une même propriété : la normalisation des démonstrations. En 1930, le théorème de complétude de Gödel montra que le critére de cohérence pouvait être vu sous différents angles. En plus de la définition précédente interne à la théorie de la démonstration, on peut également définir de manière algébrique la cohérence d'une théorie comme le fait qu'elle possède un modèle. L'équivalence entre ces deux définitions constitue un outil fondamental, qui a permis notamment la démonstration de la cohérence de nombreuses théories : la théorie des ensembles avec la négation de l'axiome du choix par Fraenkel et Mostovski, la théorie des ensembles avec l'axiome du choix et l'hypothèse du continue par Gödel, la théorie des ensembles avec la négation de l'hypothèse du continu par Cohen, . . . A l'inverse, la normalisation des démonstrations semblait ne pouvoir se définir que de manière interne à la théorie de la démonstration. Certains critères inspirés de la théorie des modèles étaient certes parfois utilisés pour démontrer la propriété de normalisation des démonstrations de certaines théories, mais la nécéssité de ces critéres n'avait pas été établie. Nous proposons dans cette thèse un critère algébrique à la fois nécessaire et suffisant pour la normalisation des démonstrations. Nous montrons ainsi que la propriété de normalisation des démonstrations peut également se définir comme un critère algébrique, à l'instar de la propriété de cohérence. Nous avons pour cela défini une nouvelle notion d'algèbre de valeurs de vérités (TVA) appelée algèbres de vérité dépendant du langage (LDTVA). La notion de TVA permet d'exhiber l'algèbre de valeurs de vérité des candidats de réductibilité définis par Girard en 1970. L'existence d'un modèle à valeurs dans cette algèbre définit un critère algébrique suffisant pour la propriété de normalisation des démonstrations. Puis nous avons défini un raffinement de la notion de candidats de réductibilité comme une de ces LDTVAs et avons montré que l'existence d'un modèle à valeurs dans cette algèbre définit un critère algébrique toujours suffisant mais également nécessaire pour la propriété de normalisation des démonstrations. Ce critère est défini pour les cadres logiques de la déduction minimale et du λΠ-calcul modulo. Et nous exhibons finalement la puissance du λΠ-calcul modulo en montrant que tous les systèmes de types purs fonctionnels peuvent être simulés dans ce cadre logique.

L'objet de cette thèse est la méta-théorie du Calcul des Constructions Inductives (CCI), c'est à dire les Calcul des Constructions étendu par des types et des prédicats inductifs. Le Calcul des Constructions a été présenté en 1985 par Thierry Coquand. Il s'agit d'un lambda-calcul typé qui, à travers l'isomorphisme dit de Curry-Howard, peut-être vu comme un formalisme logique. Ce système qui étend à la fois la logique d'ordre superieur de Church et les systèmes de Martin-Löf est particulièrement expressif du point de vue algorithmique et peut facilement être mis en oeuvre sur ordinateur.<br />Dans le Calcul des Constructions originel, les types de données (entiers, listes, sommes, etc) sont représentés dans le lambda-calcul à travers un codage imprédicatif. Cette solution est élégante mais conduit à un certain nombre de difficultés pratiques et théoriques. Pour y remédier, Thierry Coquand et Christine Paulin-Mohring on proposé d'étendre le formalisme par un mécanisme génerique de définitions inductives. C'est cette extension, utilisée dans le système Coq, qui est étudiée dans cette thèse. Le résultat essentiel est que le système vérifie bien la proprieté de normalisation forte. On en déduit les proprietés de cohérence logique, de confluence et de décidabilité du typage.<br />L'aspect le plus spectaculaire de l'extension par des types inductifs est la possibilité de définir de nouveaux types et de nouvelles propositions par récurrence structurelle (élimination forte). Cette caractéristique, qui donne toute sa signification à la notion de types dépendants, augmente énormément le pouvoir de la règle de conversion, et par là, la difficulté de la preuve de normalisation. L'interprétation de l'élimination forte dans une preuve de normalisation par réductibilité est la nouveauté essentielle de ce travail.<br />De plus, nous considérons ici un système avec eta-conversion. Une conséquence est que la propriété de confluence n'est plus combinatoire et doit être prouvée après la normalisation, ce qui augmente à nouveau la difficulté de la preuve de celle-ci. A ce titre, nous présentons également quelques résultats nouveaux sur des systèmes non-normalisants qui montrent que pour des lambda-calculs typés, la propriété de confluence est logique et non combinatoire.

Le lambda calcul avec constructeurs (de Arbiser, Miquel et Rios) est une extension du lambda calcul avec un mécanisme de filtrage. Le filtrage à la ML y est décomposé en deux étapes: une analyse de cas sur des constantes (telle l'instruction "case" de Pascal), et une commutation de l'application avec la construction de filtrage. Cette règle de commutation entre deux constructions de natures différentes induit une géométrie de calcul surprenante, a priori incompatible avec les intuitions habituelles de typage. Cependant il a été montré que ce calcul est confluent, et vérifie la propriété de séparation (à la Böhm). Cette thèse propose un système de types du polymorphique pour ce calcul, et décrit ensuite un modèle de réalisabilité, qui adapte les candidats de réductibilité de Girard au lambda calcul avec constructeurs. La normalisation forte du calcul typé et l'absence d'erreur de filtrage lors de l'évaluation en découlent immédiatement. Nous nous intéressons ensuite à la sémantique du lambda calcul avec constructeurs non typé. Une notion générique de modèle catégorique pour ce calcul est définie, puis un modèle particulier (le modèle syntaxique dans la catégorie des PERs) est construit. Nous en déduisons un résultat de complétude. Enfin, nous proposons une traduction CPS du lambda calcul avec constructeurs dans le lambda calcul simplement typé avec paires. Le lambda calcul avec constructeurs peut ainsi être simulé dans un calcul bien connu, et cette traduction nous permet aussi de transformer tout modèle par continuation en modèle du lambda calcul avec constructeurs. Une équation catégorique caractéristique de ces modèles apparait alors, qui permet de construire des modèles non syntaxiques (dans les domaines) de Scott du lambda calcul avec constructeurs.

On utilise la théorie de Floquet-Lin pour des systèmes différentiels linéaires quasi-périodiques pour établir des résultats d'existence et d'unicité et de dépendance continue des systèmes différentiels non linéaires quasi-périodiques. Et dans un second temps on établit un résultat de réductibilité d'un système différentiel linéaire presque-périodique en un système différentiel linéaire triangulaire supérieur avec conservation du nombre des solutions presque-périodiques indépendantes. Ensuite, on établit un résultat d'existence et d'unicité et de dépendance continue des systèmes différentiels non linéaires presque-périodiques par rapport au terme du contrôle.

Cette étude concerne la préparation de nouveaux matériaux pour l'élimination catalytique d'un composé organique volatil (COV) : l'acide acétique. La décomposition de cette molécule gazeuse conduit à la formation de produits nocifs tels que le CO2, l'acétone et le formaldéhyde. En présence d'oxygène, des études antérieures ont mis en évidence le caractère réfractaire de l'acide acétique en milieux aqueux. En phase gaz, la dégradation de la molécule est améliorée en présence de catalyseurs basiques et réductibles tels que les oxydes mixtes MgAl. Ces matériaux ont été synthétisés via les méthodes co-précipitation (cp) et sol-gel (sg). Sur chaque catalyseur, du cérium est déposé en surface afin d'améliorer les propriétés réductrices initiales. Les échantillons MgAlCey_cp et MgAlCey_sg (y : 0,03% ; 0,07% ; 0,14% molaire) ont montré une augmentation de la capacité de stockage de l'oxygène (CSO) et du nombre de sites basiques forts dues à la multiplicité des espèces oxygènes (O22-, O2- et/ou O2-) de surface provenant de la cérine (CeO2). En effet, la basicité et la CSO des matériaux ont augmenté pour les catalyseurs MgAlCey_sg tandis que pour MgAlCey_cp un effet de synergie apparait. La réductibilité des solides semble être indépendante du mode de préparation initial. En revanche, le nombre de sites basiques est supérieur pour les catalyseurs MgAlCey_cp par rapport à MgAlCey_sg. Cette basicité accrue des catalyseurs co-précipités leur confère une activité supérieure mais limitée par la formation supposée de carbonates au cours de la réaction d'oxydation de l'acide acétique. Hormis la cérine, la meilleure activité est obtenue par les matériaux MgAlCe0,14_cp et MgAlCe0,14_sg. / This work is devoted to the preparation of the new materials for the catalytic removal of volatile organic compound (VOC) : acetic acid. Decomposition of this gaseous molecule generate dangerous products such as CO2, acetone and formaldehyde. Removing acetic acid in aqueous phase is more difficult than gas phase. In fact, the presence of basic and redox catalysts like mixed oxides MgAl improve the oxidation of acetic acid reaction. This catalysts were prepared by co-precipitation and sol-gel methods. On each catalyst, cerium is deposited on the surface in order to improve their reducibility. MgAlCey_cp and MgAlCey_sg catalysts (y : 0.03% ; 0.07% ; 0.14% molar) have shown the increase of oxygen storage capacity (OSC) and number of strong basic sites because of various oxygen species (O22-, O2- and/or O2-) located on the surface of the materials and provided by ceria (CeO2). In fact, oxygen storage capacity of these catalysts is increased for MgAlCey_sg whereas a synergy effect appears for MgAlCey_cp. The results have shown that the reducibility of the catalysts is not related to the initial preparation method. However, basicity of MgAlCey_cp catalysts is higher than MgAlCey_sg. This basicity gives a high activity to co-precipitated catalysts which is limited by possible formation of carbonates during the oxidation reaction of acetic acid. Except for ceria, the best activity is obtained by MgAlCe0.14_cp and MgAlCe0.14_sg catalysts.

Les composés de la famille LAMOX, dérivés de La2Mo2O9, présentent une conductivité ionique élevée mais peuvent être conducteurs mixtes s'ils sont réduits sous atmosphère pauvre en oxygène. Dans ce travail, de nouvelles méthodes de synthèse de La2Mo2O9 par chimie douce (la voie sol gel et le procédé polyol) sont optimisées pour faciliter la mise en forme selon l’application souhaitée.Concernant les synthèses réalisées par voie sol gel, le composé La2Mo2O9 pur a été obtenu à partir de l’acétate de lanthane et du molybdate d’ammonium ou du chlorure de molybdène. L’influence de plusieurs paramètres de synthèse a été déterminée. L’ajout de deux tensioactifs a été testé : le bromure de diméthyldioctadécyl-ammonium (DDAB) et le F127. Les poudres finales sont quasi-pures après un traitement thermique à 950°C pendant 2 heures, ce qui ne permet pas d’avoir des surfaces spécifiques élevées.Dans le cas du procédé polyol, nous avons obtenu La2Mo2O9 pur sous forme de roses des sables par agglomération de plaquettes polycrystallines très fines constituées de cristallites de quelques dizaines de nanomètres, après un traitement thermique à plus basse température de l’ordre de 550°C. L’effet de plusieurs paramètres sur la morphologie et la pureté des poudres a été testé. En particulier, des particules sphériques agglomérées ont été obtenues en utilisant l’éthylèneglycol comme solvant en présence d’urée. L’ajout du tensioactif bromure de diméthyl-dioctadécyl-ammonium (DDAB) permet de doubler la surface spécifique par rapport aux échantillons sans tensioactif, celle ci passant de 16 à 30 m2.g-1. Finalement, de tous premiers essais ont été réalisés pour tenter d’obtenir des films minces par centrifugation.Les mesures de conductivité ont été enregistrées sur des pastilles à porosité fermée (densité relative supérieure à 92%) sans avoir recours à une étape de broyage. Les mesures de conductivité montrent que, selon les paramètres de synthèse, la conductivité de grain peut être légèrement accrue.L’étude de la réductibilité, sous H2 dilué, des poudres issues de la synthèse par voie polyol, montre que les pertes en oxygène sont plus rapides et plus importantes que pour des poudres synthétisées par voie solide. La ré-oxydation des poudres amorphes est également plus rapide et se produit à bien plus basse température dans le cas des poudres obtenues par la voie polyol. / La2Mo2O9 based oxides (LAMOX) exhibit high ionic conductivity but can be mixed conductors if they are reduced under low-oxygen atmosphere. In this work, new synthesis methods of La2Mo2O9 by soft chemistry (sol gel route and polyol process) are optimized to facilitate the sample shaping depending on the desired application.Concerning the sol gel syntheses, pure La2Mo2O9 compound was obtained from lanthanum acetate and ammonium molybdate or molybdenum chloride. The influence of several synthesis parameters was determined. The addition of two surfactants was tested: dimethyl dioctadecyl ammonium bromide (DDAB) and F127. The final powders are almost pure after heat treatment at 950 °C for 2 hours, which prevents from high specific surface areas.In the case of the polyol process, pure La2Mo2O9 was obtained as desert roses by agglomeration of very fine polycrystalline platelets built from crystallites of a few tens of nanometers size, after a heat treatment at a lower temperature of about 550°C. The effect of various parameters on the morphology and purity of the powder was tested. In particular, agglomerated spherical particles have been obtained using ethylene glycol as solvent in the presence of urea. The addition of DDAB surfactant enables a doubling the specific surface area comparatively to samples without surfactant, from 16 to 30 m2.g-1. Finally, first tests were carried out as attempts to obtain thin films by centrifugation.Conductivity measurements were recorded on pellets presenting closed porosity (relative density greater than 92%), obtained without the help of a milling step. Conductivity measurements showed that, depending on the synthesis parameters, the grain conductivity can be slightly increased.The study of the reducibility, under diluted H2, of powders resulting from the synthesis by the polyol process, shows that the oxygen losses are faster and larger than with powders synthesized by solid state reaction. Reoxidation of amorphous powders is also faster and occurs at much lower temperature in the case of powders obtained by the polyol pathway.

Ce travail est relatif à la synthèse et à la caractérisation d'oxydes mixtes Pr1-zCezO2-y et Pr1-xZrxO2-y. Différentes compositions chimiques associées à une valence mixte Pr4+/Pr3+ concomitant à un taux précis de lacunes d'oxygènes ont été isolées tant pour les composés à l'état oxydé que pour ces derniers réduits sous Ar/H2. A l'état réduit, différentes surstructures de la maille fluorine ont été caractérisées par diffraction des RX et de neutrons. Sur la base de mesures magnétiques, d'analyses par spectroscopie d'absorption X (XANES-EXAFS) aux seuils K du Zr et LIII du Ce/Pr et d'analyses thermogravimétriques et/ou TPR (Temperature Programmed Reduction), les évolutions des taux de Pr4+/Pr3+ dans cette série ont été déterminées. Enfin, des mesures in-situ sous atmosphère réductrice par diffraction de neutrons et EELS (Electron Energy Loss Spectroscopy) ont été réalisées dans l'objectif de corréler compositions chimiques- édifices structuraux et propriétés de réductibilité.

Le lambda calcul avec constructeurs (de Arbiser, Miquel et Rios) est une extension du lambda calcul avec un mécanisme de filtrage. Le filtrage à la ML y est décomposé en deux étapes: une analyse de cas sur des constantes (telle l'instruction «case» de Pascal), et une commutation de l'application avec la construction de filtrage. Cette règle de commutation entre deux constructions de natures différentes induit une géométrie de calcul surprenante, a priori incompatible avec les intuitions habituelles de typage. Cependant il a été montré que ce calcul est confluent, et vérifie la propriété de séparation (à la Böhm). Cette thèse propose un système de types du polymorphique pour ce calcul, et décrit ensuite un modèle de réalisabilité, qui adapte les candidats de réductibilité de Girard au lambda calcul avec constructeurs. La normalisation forte du calcul typé et l'absence d'erreur de filtrage lors de l'évaluation en découlent immédiatement. Nous nous intéressons ensuite à la sémantique du lambda calcul avec constructeurs non typé. Une notion générique de modèle catégorique pour ce calcul est définie, puis un modèle particulier (le modèle syntaxique dans la catégorie des PERs) est construit. Nous en déduisons un résultat de complétude. Enfin, nous proposons une traduction CPS du lambda calcul avec constructeurs dans le lambda calcul simplement typé avec paires. Le lambda calcul avec constructeurs peut ainsi être simulé dans un calcul bien connu, et cette traduction nous permet aussi de transformer tout modèle par continuation en modèle du lambda calcul avec constructeurs. Une équation catégorique caractéristique de ces modèles apparait alors, qui permet de construire des modèles non syntaxiques (dans les domaines) de Scott du lambda calcul avec constructeurs. / The lambda calculus with constructors was introduced by Arbiser, Miquel and Rios in the early 2000's as an extension of lambda calculus with pattern matching features. It decomposes the pattern matching à la ML into a case-analysis on constant constructors (in the spirit of the case instruction in Pascal), and a commutation rule between case construction and application. This commutation rule between two different kinds of constructions designs a surprising computational behaviour, a priori} not compatible with usual typing intuitions. However the whole calculus was proved confluent, and it enjoys the separation property (a version of Böhm's lemma).In this thesis we propose a polymorphic type system for this calculus, and we develop a realisability model, based on Girard's reducibility candidates. This leads to a strong normalisation result for the typed calculus, and guaranties that the type system prevents match failure. Next we focus on semantics for the untyped calculus. We first define a generic notion of models for the lambda calculus with constructors in Cartesian closed categories. We then establish the syntactic model in the category of PERs, and deduce a completeness result from it.Finally, we consider a translation of the lambda calculus with constructors into the pure lambda lambda calculus relying on continuation passing style techniques. This enables the simulation of the lambda calculus with constructors by a well known calculus, and provides a transformation of every continuation model into a model of the lambda calculus with constructors. Thereby a categorical equation characteristic of these models appears, which enables the construction of non syntactic models in Scott's domains.