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.

L’identification des micro-organismes reposait jusqu’à présent sur l’étude des caractères culturaux et biochimiques de chaque espèce. Depuis quelques années, la spectrométrie de masse de type Matrix Assisted Laser Desorption/Ionization Time Of Flight (MALDI-TOF) s’est développée dans les laboratoires de microbiologie clinique. Cette nouvelle technologie permet de réaliser très rapidement et à moindre coût un diagnostic d’espèce sur des colonies de bactéries ou de champignons isolées sur des milieux de culture solides.Dans un premier temps, nous avons montré que cette technologie permet de réaliser une identification des germes isolés en milieu liquide, comme les flacons d’hémoculture au cours des bactériémies par exemple. Ce dépistage se fait directement à partir du flacon positif, sans attendre l’isolement des colonies sur milieu solide. Ce diagnostic disponible dès le premier jour permet d’adapter l’antibiothérapie au phénotype de résistance habituel de l’espèce.Dans un deuxième temps, nous avons cherché à identifier la nature des biomarqueurs utilisés pour l’identification des espèces bactériennes, en prenant comme exemple la bactérie pathogène Neisseria meningitidis. La comparaison du génome et du protéome des souches entièrement séquencées a permis de mettre en évidence la nature exacte des protéines impliquées dans le diagnostic d’espèce. Par ailleurs, les protéines ribosomales étant majoritaires et pouvant servir d’outil épidémiologique, nous avons constaté que la mise en évidence de leurs variations sur le spectre de masse rend la différenciation de souches au sein d’une même espèce possible, en adaptant la méthode d’analyse. Enfin, nous avons présenté des résultats préliminaires encourageants sur l’exploitation du caractère constant de certaines protéines ribosomales visibles directement sur le spectre de masse, permettant de différencier des espèces très proches, comme Streptococcus pneumoniae et Streptococcus mitis. / Until now, bacterial and fungal identification has been based on biochemical characterization of microorganisms. The Matrix-Assisted Laser Desorption/Ionization Time of Flight Spectrometry (MALDI-TOF MS) has recently been developed in clinical microbiology laboratories. This new technology allows a rapid, accurate and less expensive identification of bacterial and fungal colonies grown on agar media. First, we have shown that the direct identification of bacteria grown in liquid media such as blood cultures was possible, without waiting for a subculture on solid media. Since the diagnosis is available on the first day, the presumptive antimicrobial treatment can be rapidly adapted according to the usual resistance phenotype of the microorganism. We have then searched to identify the biomarkers used for the identification of bacteria, using Neisseria meningitidis as a model. Comparing the genome and the proteome of sequenced strains allowed us to identify the ribosomal proteins as thoses involved in the MALDI-TOF MS diagnosis. Ribosomal proteins are very abundant and are very often used as epidemiological tools : their variations on the bacteria mass spectrum allows an intra-species differentiation of several strains. Finally we present encouraging preliminary results based on the detection of consistent ribosomal proteins directly visible on the mass spectrum that lead to the accurate identification of some very close species such as Streptococcus pneumoniae and Streptococcus mitis.

Exprimer le parallélisme dans la programmation de manière simple et performante est un défi auquel l'informatique fait face, en raison de l'évolution actuelle des architectures matérielles. BSML est un langage permettant une programmation parallèle de haut niveau, structurée, qui participe à cette recherche. En s'appuyant sur le coeur du langage existant, cette thèse propose d'une part des extensions qui en font un langage plus général et plus simple (traits impératifs tels que références et exceptions, syntaxe spécifique...) tout en conservant et étendant sa sûreté (sémantiques formelles, système de types...) et d'autre part une méthodologie de développement d'applications parallèles certifiées / Finding a good paradigm to represent parallel programming in a simple and efficient way is a challenge currently faced by computer science research, mainly due to the evolution of machine architectures towards multi-core processors. BSML is a high level, structured parallel programming language that takes part in the research in an original way. By building upon existing work, this thesis extends the language and makes it more general, simple and usable with added imperative features such as references and exceptions, a specific syntax, etc. The existing formal and safety characteristics of the language (semantics, type system...) are preserved and extended. A major application is given in the form of a methodology for the development of fully proved parallel programs

La vérification déductive de programmes consiste à annoter des programmes par une spécification, c'est-à-dire un ensemble de formules logiques décrivant le comportement du programme, et à prouver que les programmes vérifient bien leur spécification. Des outils tels que la plate-forme Why prennent en entrée un programme et sa spécification et calculent des formules logiques telles que, si elles sont prouvées, le programme vérifie sa spécification. Ces formules logiques peuvent être prouvées automatiquement ou à l'aide d'assistants de preuve.Lorsqu'un programme est écrit dans un langage supportant les alias de pointeurs, c'est-à-dire si plusieurs variables peuvent désigner la même case mémoire, alors le raisonnement sur le programme devient particulièrement ardu. Il est nécessaire de spécifier quels pointeurs peuvent être égaux ou non. Les invariants des structures de données, en particulier, sont plus difficiles à vérifier.Cette thèse propose un système de type permettant de structurer la mémoire de façon modulaire afin de contrôler les alias de pointeurs et les invariants de données. Il est basé sur les notions de région et de permission. Les programmes sont ensuite interprétés vers Why de telle façon que les pointeurs soient séparés au mieux, facilitant ainsi le raisonnement. Cette thèse propose aussi un mécanisme d'inférence permettant d'alléger le travail d'annotation des opérations de régions introduites par le langage. Un modèle est introduit pour décrire la sémantique du langage et prouver sa sûreté. En particulier, il est prouvé que si le type d'un pointeur affirme que celui-ci vérifie son invariant, alors cet invariant est effectivement vérifié dans le modèle. Cette thèse a fait l'objet d'une implémentation sous la forme d'un outil nommé Capucine. Plusieurs exemples ont été écrits pour illustrer le langage, et ont été vérifié à l'aide de Capucine. / Deductive verification consists in annotating programs by a specification, i.e. logic formulas which describe the behavior of the program, and prove that programs verify their specification. Tools such as the Why platform take a program and its specification as input and compute logic formulas such that, if they are valid, the program verifies its specification. These logic formulas can be proven automatically or using proof assistants.When a program is written in a language supporting pointer aliasing, i.e. if several variables may denote the same memory cell, then reasoning about the program becomes particularly tricky. It is necessary to specify which pointers may or may not be equal. Invariants of data structures, in particular, are harder to maintain.This thesis proposes a type system which allows to structure the heap in a modular fashion in order to control pointer aliases and data invariants. It is based on the notions of region and permission. Programs are then translated to Why such that pointers are separated as best as possible, to facilitate reasoning. This thesis also proposes an inference mechanism to alleviate the need to write region operations introduced by the language. A model is introduced to describe the semantics of the language and prove its safety. In particular, it is proven that if the type of a pointer tells that its invariant holds, then this invariant indeed holds in the model. This work has been implemented as a tool named Capucine. Several examples have been written to illustrate the language, and where verified using Capucine.

L'objet de cette thèse est l'extension des méthodes de la théorie des types intersections non-idempotents, introduite par Gardner et de Carvalho, à des cadres dépassant le lambda-calcul stricto sensu.- Nous proposons d'abord une caractérisation de la normalisation de tête et de la normalisation forte du lambda-mu calcul (déduction naturelle classique) en introduisant des types unions non-idempotents. Comme dans le cas intuitionniste, la non-idempotence nous permet d'extraire du typage des informations quantitatives ainsi que des preuves de terminaison beaucoup plus élémentaires que dans le cas idempotent. Ces résultats nous conduisent à définir une variante à petits pas du lambda-mu-calcul, dans lequel la normalisation forte est aussi caractérisée avec des méthodes quantitatives. - Dans un deuxième temps, nous étendons la caractérisation de la normalisation faible dans le lambda-calcul pur à un lambda-calcul infinitaire étroitement lié aux arbres de Böhm et dû à Klop et al. Ceci donne une réponse positive à une question connue comme le problème de Klop. À cette fin, il est nécessaire d'introduire conjointement un système (système S) de types infinis utilisant une intersection que nous qualifions de séquentielle, et un critère de validité servant à se débarrasser des preuves dégénérées auxquelles les grammaires coinductives de types donnent naissance. Ceci nous permet aussi de donner une solution au problème n°20 de TLCA (caractérisation par les types des permutations héréditaires). Il est à noter que ces deux problèmes n'ont pas de solution dans le cas fini (Tatsuta, 2007).- Enfin, nous étudions le pouvoir expressif des grammaires coinductives de types, en dehors de tout critère de validité. Nous devons encore recourir au système S et nous montrons que tout terme est typable de façon non triviale avec des types infinis et que l'on peut extraire de ces typages des informations sémantiques comme l'ordre (arité) de n'importe quel lambda-terme. Ceci nous amène à introduire une méthode permettant de typer des termes totalement non-productifs, dits termes muets, inspirée de la logique du premier ordre. Ce résultat prouve que, dans l'extension coinductive du modèle relationnel, tout terme a une interprétation non vide. En utilisant une méthode similaire, nous montrons aussi que le système S collapse surjectivement sur l'ensemble des points de ce modèle. / In this dissertation, we extend the methods of non-idempotent intersection type theory, pioneered by Gardner and de Carvalho, to some calculi beyond the lambda-calculus.- We first present a characterization of head and strong normalization in the lambda-mu calculus (classical natural deduction) by introducing non-idempotent union types. As in the intuitionistic case, non-idempotency allows us to extract quantitative information from the typing derivations and we obtain proofs of termination that are far more elementary than those in the idempotent case. These results leads us to define a small-step variant of the lambda-mu calculus, in which strong normalization is also characterized by means of quantitative methods.- In the second part of the dissertation, we extend the characterization of weak normalization in the pure lambda-calculus to an infinitary lambda-calculus narrowly related to Böhm trees, which was introduced by Klop et al. This gives a positive answer to a question known as Klop's problem. In that purpose, it is necessary to simultaneously introduce a system (system S) featuring infinite types and resorting to an intersection operator that we call sequential, and a validity criterion in order to discard unsound proofs that coinductive grammars give rise to. This also allows us to give a solution to TLCA problem #20 (type-theoretic characterization of hereditary permutations). It is to be noted that those two problem do not have a solution in the finite case (Tatsuta, 2007).- Finally, we study the expressive power of coinductive type grammars, without any validity criterion. We must once more resort to system S and we show that every term is typable in a non-trivial way with infinite types and that one can extract semantical information from those typings e.g. the order (arity) of any lambda-term. This leads us to introduce a method that allows typing totally unproductive terms (the so-called mute terms), which is inspired from first order logic. This result establishes that, in the coinductive extension of the relational model, every term has a non-empty interpretation. Using a similar method, we also prove that system S surjectively collapses on the set of points of this model

Le système de types de la logique d'ordre supérieur permet d'exclure certaines expressions indésirables telles que l'application d'un prédicat à lui-même. Cependant, il ne suffit pas pour vérifier des critères plus complexes comme l'absence de divisions par zéro. Cette thèse est consacrée à l’étude d’une extension de la logique d’ordre supérieur appelée sous-typage par prédicats (predicate subtyping), dont l'objet est de rendre l'attribution de types aussi expressive que l'attribution de prédicats. A partir d'un type A et d'un prédicat P(x) de domaine A, le sous-typage par prédicats permet de construire un sous-type de A, noté {x : A | P(x)}, dont les éléments sont les termes t de type A tels que P(t) est démontrable. Le sous-typage par prédicats est au coeur du système PVS.Ce travail présente la formalisation d'un système minimal incluant le sous-typage par prédicats, appelé PVS-Core, ainsi qu'un système de certificats vérifiables pour PVS-Core. Ce deuxième système, appelé PVS-Cert, repose sur l'introduction de termes de preuves et de coercions explicites. PVS-Core et PVS-Cert sont munis d'une notion de conversion correspondant respectivement à l'égalité modulo beta et à l'égalité modulo beta et effacement des coercions, choisi pour établir une correspondance simple entre les deux systèmes.La construction de PVS-Cert est semblable à celle des PTS (Pure Type Systems) avec paires dépendantes et PVS-Cert peut être muni de la notion de beta-sigma-réduction utilisée au coeur de ces systèmes. L'un des principaux théorèmes démontré dans ce travail est la normalisation forte de la réduction sous-jacente à la conversion et de la beta-sigma-réduction. Ce théorème permet d'une part de construire un algorithme de vérification du typage (et des preuves) pour PVS-Cert et d'autre part de démontrer un résultat d'élimination des coupures, utilisé à son tour pour prouver plusieurs propriétés importantes des deux systèmes étudiés. Par ailleurs, il est également démontré que PVS-Cert est une extension conservative du PTS lambda-HOL, et qu'en conséquence PVS-Core est une extension conservative de la logique d'ordre supérieur.Une deuxième partie présente le prototype d'une instrumentation de PVS pour produire des certificats de preuve. Une troisième et dernière partie est consacrée à l'étude de liens entre logique classique et constructive avec la définition d'une traduction par double négation minimale ainsi que la présentation d'un algorithme de constructivisation automatique des preuves. / The type system of higher-order logic allows to exclude some unexpected expressions such as the application of a predicate to itself. However, it is not sufficient to verify more complex criteria such as the absence of divisions by zero. This thesis is dedicated to the study of an extension of higher-order logic, named predicate subtyping, whose purpose is to make the assignment of types as expressive as the assignment of predicates. Starting from a type A and a predicate P(x) of domain A, predicate subtyping allows to build a subtype of A, denoted {x : A | P(x)}, whose elements are the terms t of type A such that P(t) is provable. Predicate subtyping is at the heart of the proof system PVS.This work presents the formalization of a minimal system expressing predicate subtyping, named PVS-Core, as well as a system of verifiable certificates for PVS-Core. This second system, named PVS-Cert, is based on the introduction of proof terms and explicit coercions. PVS-Core and PVS-Cert are equipped with a notion of conversion corresponding respectively to equality modulo beta and to equality modulo beta and the erasure of coercions, chosen to establish a simple correspondence between the two systems.The construction of PVS-Cert is similar to that of PTSs (Pure Type Systems) with dependent pairs and PVS-Cert can be equipped with the notion of beta-sigma-reduction used at the core of these systems. One of the main theorems proved in this work is the strong normalization of both the reduction underlying the conversion and beta-sigma-reduction. This theorem allows, on the one hand, to build a type-checking (and proof-checking) algorithm for PVS-Cert and, on the other hand, to prove a cut elimination result, used in turn to prove important properties of the two studied systems. Furthermore, it is also proved that PVS-Cert is a conservative extension of the PTS lambda-HOL and that, as a consequence, PVS-Core is a conservative extension of higher-order logic.A second part presents the prototype of an instrumentation of PVS to generate proof certificates. A third and final part is dedicated to the study of links between classical and constructive logic, with the definition of a minimal double-negation translation as well as the presentation of an automated proof constructivization algorithm.

L’objectif de ces travaux de thèse a été de contribuer à la compréhension de la physiopathologie des infections sur matériel ostéo-articulaire (IMOA) à C. acnes. Dans un premier temps, nous avons typé par MLST 108 isolats de C. acnes responsables de 34 cas d’IMOAs monomicrobiennes et corrélé les résultats de typage aux données clinico-biologiques. Nous avons ainsi montré que les IMOAs à C. acnes correspondent à 2 entités cliniques : i) les cas « homotypiques » qui sont des vraies infections dues à un clone de C. acnes responsable d’une réponse inflammatoire de l’hôte ii) les cas hétérotypiques qui sont une colonisation ou contamination itérative du matériel ostéo-articulaire en l’absence de réponse inflammatoire de l’hôte. Ces données de typage ont souligné les limites de la définition microbiologique actuelle d’une IMOA quand il s’agit de C. acnes et la nécessité d’intégrer un outil moléculaire fiable dans le diagnostic microbiologique de routine de ces infections. Nous avons par conséquent évalué la technique SLST développée pour un typage rapide et optimal de C. acnes en routine. Le pouvoir discriminant de cette technique était insuffisant suggérant que seule la mise en place du NGS en temps réel dans les laboratoires de microbiologie pourrait répondre au besoin de typage moléculaire pour améliorer le diagnostic microbiologique de ces infections.Nos résultats de typage ont montré que la clonalité de l’infection plutôt que le complexe clonal (CC) est le principal facteur déterminant du processus physiopathologique et inflammatoire de l’IMOA à C. acnes. Cette conclusion est concordante avec les résultats que nous avons obtenus dans un modèle in vitro d’infection de macrophages THP-1 par C. acnes. Grâce à ce modèle, nous avons pu montrer que la réponse inflammatoire in vitro de nos isolats est souche –et non CC– dépendante. De plus, les réponses inflammatoires in vitro et in vivo n’étaient pas corrélées. Ceci souligne les limites des modèles in vitro dans l’étude de la physiopathologie des IMOAs à C. acnes dans lesquels l’adaptation de la bactérie à l’hôte est complètement négligée lors de l’étude de la réponse immune. Dans la dernière partie de ce travail, nous avons confirmé l’importance de l’environnement dans le conditionnement du comportement de la bactérie. Nous avons mené une étude comparative des caractéristiques culturales ex vivo et ex vitro de nos isolats de C. acnes. Nous avons montré l’impact du CC et des conditions environnementales, par extension la pression que peut exercer l’hôte, sur le profil cultural de C. acnes. En conclusion, nos travaux montrent qu’une approche multifactorielle, intégrant à la fois la génomique et la réponse de l’hôte, est nécessaire pour comprendre la physiopathologie des IMOAs à C. acnes. / The aim of this thesis was to contribute to the understanding of the physiopathology of C. acnes orthopedic-device related infections (ODRI). Firstly, we typed by MLST 108 C. acnes isolates responsible for 34 cases of monomicrobial ODRIs and correlated typing results with bio-clinical data. We have shown that C. acnes ODRIs correspond to two clinical entities: i) "homotypic" cases corresponding to true infections with a single pathogenic clone of C. acnes eliciting an inflammatory response ii) heterotypic cases corresponding to colonization or iterative contamination of the implant without systemic inflammatory response. These typing data highlighted the limitations of the current microbiological definition of ODRI when it comes to C. acnes and the need to incorporate a reliable molecular tool into the routine microbiological diagnosis of these infections. We therefore evaluated the SLST technique developed for a rapid and optimal typing of C. acnes. The discriminating power of this technique was insufficient suggesting that only the establishment of real-time NGS in microbiology laboratories could improve the microbiological diagnosis. Our typing results showed that the clonal status of the infection and not CC is the main determining factor in the physiopathological and inflammatory process of C. acnes ODRI. This conclusion is consistent with our results obtained on an in vitro model of a macrophage THP-1 infection. Using this model, we have shown that the in vitro inflammatory response of our isolates is strain- and non-CC-dependent. In addition, the in vitro and in vivo inflammatory responses were not correlated. This underscores the limitations of in vitro models in the study of C. acnes ODRIs in which the adaptation of the bacteria to the host is completely neglected during the study of the immune response. Finally, we confirmed the importance of the environment in the conditioning of the behavior of the bacterium. We conducted a comparative study of the ex vivo and ex vitro growth characteristics of our C.acnes isolates. We have shown the impact of CC and environmental conditions, by extension the pressure that can exert the host, on the cultural profile of C. acnes. In conclusion, our work shows that a multifactorial approach, integrating both genomics and host response, is needed to understand the physiopathology of C. acnes ODRI.

Cette thèse s'intéresse à la modélisation de la syntaxe et de l'interface syntaxe-sémantique de la phrase, et explore la possibilité de contrôler au niveau des structures de dérivation la surgénération que produit le traitement des dépendances à distance par des types d'ordre supérieur. À cet effet, nous étudions la possibilité d'étendre le système de typage des Grammaires Catégorielles Abstraites avec les constructions de la somme disjointe, du produit cartésien et du produit dépendant, permettant d'étiqueter les catégories syntaxiques par des structures de traits. Nous prouvons dans un premier temps que le calcul résultant de cette extension bénéficie des propriétés de confluence et de normalisation, permettant d'identifier les termes beta-équivalents dans le formalisme grammatical. Nous réduisons de plus le même problème pour la beta-eta-équivalence à un ensemble d'hypothèse de départ. Dans un second temps, nous montrons comment cette introduction de structures de traits peut être appliquée au contrôle des dépendances à distances, à travers les exemples des contraintes de cas, des îlots d'extraction pour les mouvements explicites et implicites, et des extractions interrogatives multiples, et nous discutons de la pertinence de placer ces contrôles sur les structures de dérivation.

Cette thèse concerne la combinaison du lambda-calcul et de la réécriture, dont nous étudions principalement deux propriétés : la confluence et la normalisation forte. Nous commençons par étudier sous quelles conditions la combinaison d'une relation de réécriture conditionnelle confluente au lambda-calcul donne une relation de réécriture confluente. Ensuite nous nous intéressons aux preuves de normalisation forte de lambda-calculs typés utilisant la technique de réductibilité. Notre contribution la plus importante est une comparaison de diverses variantes de cette technique, utilisant comme outil de comparaison la manière dont ces variantes s'étendent à la réécriture et dont elles prennent en compte les types unions et les types existentiels implicites. Enfin, nous présentons un critère, basé sur un système de types contraints, pour la normalisation forte de la réécriture conditionnelle combinée au lambda-calcul. Notre approche étend des critères de terminaison existants qui utilisent des annotations de taille. C'est à notre connaissance le premier critère de terminaison pour la réécriture conditionnelle avec membres droits d'ordre supérieur qui prenne en compte, dans l'argument de terminaison, de l'information issue de la satisfaction des conditions des règles de réécriture / This thesis is about the combination of lambda-calculus with rewriting. We mainly study two properties: confluence and strong normalization. We begin by studying under which conditions the combination of a confluent conditional rewrite relation to the lambda-calculus leads to a confluent relation. Next, we study strong normalization proofs of typed lambda-calculi that use the reducibility technique. Our main contribution is a comparison of variants of this technique, with respect to how they extend to rewriting and how they handle union and implicit existential types. Finally, we present a termination criterion for the combination of conditional rewriting and lambda-calculus based on a constrained type system. Our approach, which extends known criteria that use sized types, is to our knowledge the first termination criterion for conditional rewriting with higher-order right-hand sides that takes into account in the termination argument some information generated by the satisfaction of the conditions of the rewrite rules

L’objectif de mon travail fut de valider et d’optimiser la spectrométrie de masse de type MALDI-TOF pour l’identification et la classification d'un ensemble de bactéries pathogènes ou opportunistes chez l’homme, en enrichissant une base de données et en testant la robustesse de la méthode, afin d’obtenir une méthode rapide fixe et fiable d'acquisition de résultats. Les différents résultats obtenus ont permis la validation de la technique comme outil d’identification bactérienne fiable en routine. Elle permet désormais de caractériser les mélanges de deux bactéries voir même la différentiation d’espèces très proches comme les Shigella spp et E. coli. Nous avons montré que la technique sera encore améliorée par un outil supplémentaire de comparaison des souches pour une veille épidémiologique "en temps réel", sans investissement supplémentaire, en permettant plusieurs types d'économie. Elle apporte un gain réel dans la prise en charge du patient et le choix éclairé des antibiotiques testés pour l'antibiogramme. La technique peut aussi constituer un outil alternatif de sérotypage. / The aim of this work was to validate and optimize MALDI-TOF mass spectrometry for the identification and classification of a set of pathogens or opportunistic bacteria, by enriching a database and testing the robustness of the method, in order to obtain a quick and reliable fixed acquisition results. The different results obtained allowed the validation of the technique as a reliable tool for bacterial identification in hospital routine. In addition, we have shown that it can characterize mixtures of two bacteria and differentiate closely related species such as Shigella spp and E. coli. We demonstrate that MALDI-TOF/MS will be further enhanced by an additional tool for comparison of strains for epidemiological monitoring in "real time". The technique can also be an alternative tool for serotyping. MALDI-TOF/MS identification provides a real benefit in terms of patient care and the choice of antibiotics tested for sensitivity, without additional investment, which allows different types of economy.