La théorie des types est une discipline au croisement de la logique, des mathématiques et de l'informatique. Elle peut servir de support au développement de programme "zéro faute". L'objet de cette thèse est d'étudier l'extension d'un système aux types dépendants UTT (comprenant notamment des types inductifs) par une relation de récriture concernant un fragment du calcul, à savoir les types finis. Nous nous assurons d'abord que les propriétés de normalisation forte, de confluence et de préservation du type sont toujours préservées malgré l'ajout de la réduction. Ensuite nous enrichissons ce système par la notion de sous-typage coercitif vue comme un mécanisme d'abréviation et effectuons la preuve de conservativité pour le système enrichi du sous-typage par rapport au système de base. L'intérêt d'un tel système est qu'il améliora l'efficacité des assistants à la preuve et offrira un bon cadre pour l'étude des problèmes faisant intervenir des ensembles finis (combinatoire, manipulation de graphe etc).

Dans le domaine de l'ingénierie du logiciel, les systèmes de types sont souvent considérés pour la prévention de l'occurrence de termes dénués de sens par rapport à une spécification des types. Dans le cadre de l'extension d'un langage de programmation avec des caractéristiques dédiées, le typage de ces dernières doit être compatible avec les caractéristiques du langage hôte. Cette thèse se situe dans le contexte de la réécriture de termes embarquée dans la programmation orientée objet. Elle vise à développer un système de types avec sous-typage pour le support du filtrage de motifs associatif sur des termes algébriques construits sur des opérateurs variadiques. Ce travail s'appuie sur le langage de réécriture Tom qui fournit des constructions de filtrage de motifs et des stratégies de réécriture à des langages généralistes comme Java. Nous décrivons l'évaluation de code Tom à travers la définition de la sémantique opérationnelle de ce langage en tant qu'élément essentiel de la preuve de la sûreté du système de types. Celui-ci inclut la vérification de types ainsi que l'inférence de types à base de contraintes. Le langage de contraintes est composé d'une part, de contraintes d'égalité, résolues par unification, d'autre part, de contraintes de sous-typage, résolues par la combinaison de phases de simplification, de génération d'une solution et de ramassage de miettes. Le système de types a été intégré au langage Tom, ce qui permet une plus forte expressivité et plus de sûreté a fin d'assurer que les transformations décrites par des règles de réécriture préservent le type des termes.

Dans le domaine de l'ingénierie du logiciel, les systèmes de types sont souvent considérés pour la prévention de l'occurrence de termes dénués de sens par rapport à une spécification des types. Dans le cadre de l'extension d'un langage de programmation avec des caractéristiques dédiées, le typage de ces dernières doit être compatible avec les caractéristiques du langage hôte. Cette thèse se situe dans le contexte de la réécriture de termes embarquée dans la programmation orientée objet. Elle vise à développer un système de types avec sous-typage pour le support du filtrage de motifs associatif sur des termes algébriques construits sur des opérateurs variadiques. Ce travail s'appuie sur le langage de réécriture Tom qui fournit des constructions de filtrage de motifs et des stratégies de réécriture à des langages généralistes comme Java. Nous décrivons l'évaluation de code Tom à travers la définition de la sémantique opérationnelle de ce langage en tant qu'élément essentiel de la preuve de la sûreté du système de types. Celui-ci inclut la vérification de types ainsi que l'inférence de types à base de contraintes. Le langage de contraintes est composé d'une part, de contraintes d'égalité, résolues par unification, d'autre part, de contraintes de sous-typage, résolues par la combinaison de phases de simplification, de génération d'une solution et de ramassage de miettes. Le système de types a été intégré au langage Tom, ce qui permet une plus forte expressivité et plus de sûreté a fin d'assurer que les transformations décrites par des règles de réécriture préservent le type des termes / In software engineering, type systems are often considered in order to prevent the occurrence of meaningless terms in regard to a type specification. When extending a given programming language with new dedicated features, the typing of these features must be compatible with the ones in the host language. This thesis is situated in the context of term rewriting embedded in object-oriented programming and aims to develop a safe type system featuring subtyping for the support of associative pattern matching on algebraic terms built from variadic operators. In this work we consider the Tom rewriting language that provides associative pattern matching constructs and rewrite strategies for Java. We describe Tom code evaluation through the definition of the operational semantics of the Tom language as an essential element to show that the type system is safe. The type system includes type checking and constraint-based type inference. The constraint language is composed of equality constraints solved by unification and subtyping constraints solved by a combination of simplification, generation of solution and garbage collecting. The type system was integrated in Tom which provides both stronger expressiveness and more safety able to ensure that the transformations described by rewrite rules preserve the type of terms

Les langages à objets offrent une forme particulière de polymorphisme en permettant l'écriture de « méthodes » dont l'exécution dépend du type dynamique des arguments. Ce « dispatch dynamique » ne prend généralement en compte qu'un argument unique. Certains langages permettent le dispatch simultané sur tous les arguments et on parle alors de « multi-méthodes ». Cette thèse s'intéresse à la définition et au typage d'un langage dérivant de ML avec multiméthodes. Celles-ci sont introduites comme un cas particulier de filtrage sur les objets. La présentation du système de types utilise une approche algébrique. Plutôt que de figer l'ensemble des types, on en axiomatise les propriétés nécessaires pour la correction du système. Cela permet d'écrire des preuves génériques qui ne dépendent pas du choix de l'algèbre. On montre ainsi comment réduire la vérification automatique du typage à la résolution de problèmes simples du premier ordre (contraintes). La résolution des problèmes de contraintes peut alors réutiliser le corpus de résultats disponibles dans la littérature. L'avantage de cette approche algébrique est qu'elle permet de traiter d'un coup toute une classe de langages possibles se distinguant par la nature de l'algèbre de types, du langage d'expression des contraintes et du modèle d'interprétation de ces contraintes. Elle offre également un outil intéressant pour étudier le typage dans un contexte où le monde d'interprétation est ouvert, c'est-à-dire quand on souhaite que le typage d'un module apporte une garantie pour toutes les utilisations possibles de ce module.

Le calcul réparti est de plus en plus utilisé bien qu'il reste très mal maîtrisé. Cette thèse porte sur le Dpi-calcul, une extension simple du pi-calcul dans laquelle tous les processus sont placés dans des localités afin de décrire leur répartition. Dans ce calcul, les processus peuvent communiquer localement et migrer entre localités. À côté des canaux de communication et des localités, on identifie une nouvelle famille d'identifiants, les passeports, permettant un contrôle fin des migrations de processus : un processus doit disposer d'un passeport adéquat pour entrer dans une localité.<br /><br />Afin de structurer le calcul, on met en place un système de types qui associe un type à chaque identifiant pour vérifier qu'un processus n'utilise que les droits qu'il possède. L'ordre de sous-typage sur les types est étendu aux types de passeports suivant les localités d'origine des processus migrant. On démontre que cet ordre admet des bornes inférieures sous certaines conditions. On prouve également que les processus se conformant à cette politique de typage conservent cette propriété au cours de leurs réductions.<br /><br />On étudie aussi l'équivalence observationnelle : quand des processus exhibent-ils des comportements indiscernables pour un observateur ? En présence de passeports, il est indispensable d'imposer à l'observateur d'être loyal, c'est-à-dire d'exiger la possession de passeports pour observer les communications ayant lieu dans les localités correspondantes. Ces contraintes définissent une congruence dite barbue loyale. On développe ensuite un système de transitions étiquetées tel que la bisimilarité loyale engendrée coïncide avec cette congruence barbue loyale.

Cette thèse porte sur l'étude théorique et pratique d'un système de typage appliqué à la preuve de programmes de style fonctionnels. Le système de base est le système ST créé par C.Raffalli; il comporte, outre le polymorphisme, du sous-typage et de l'omission de contenu non-algorithmique. Nous étudions tout d'abord les modèles de la théorie définie par le système de types, en construisant une axiomatique basée sur les treillis permettant de modéliser le calcul et la logique. Nous étudions sur cette base le système de types, montrons la réduction du sujet, et la possibilité de définir en interne la normalisabilité et la réductibilité des programmes. Dans la suite de la thèse, plus appliquée, nous étudions des codages de types de données riches inspirés des langages fonctionnels - y incluant notamment un système de modules du premier ordre- dans le Lambda-Calcul, et montrons qu'ils s'intègrent harmonieusement dans le système; la méthodologie développée dans cette partie permet d'étendre le langage de types et le langage de programmation en conservant un critère de consistance assurant la sûreté du code typé.

XML (eXtensible Markup Language) est un format standard pour l'échange de données semi-structurées, qui est utilisé dans services web, les bases de données, et comme format de sérialisation pour échanger des données entre applications. Afin d'avoir un meilleur traitement de données XML, plusieurs langages statiquement typés pour XML ont été récemment définis, tels XDuce, CDuce, XJ, XTatic, XACT, XHaskell, OCamlDuce. Ces langages peuvent vérifier si un programme n'engendra d'erreurs de types à l'exécution. Mais la plupart de ces langages n'incluent pas le polymorphisme paramétrique ou l'incluent sous un forme très limitée. Cependant, le traitement de données XML nécessite du polymorphisme paramétrique, c'est pourquoi il a été demandé et discuté à plusieurs reprises dans diverses groupes de travail de standardisation (par example, RELAX-NG et XQuery). Nous étudions dans cette thèse les techniques pour étendre par le polymorphisme paramétrique les langages de traitement XML. Notre solution se deroule sur deux étapes: (i) nous définissons et étudions une relation de sous-typage polymorphe sémantique pour un système de type avec types récursifs, types des produits, types des flèches, et types des ensemblistes (c'est-à-dire, l'union, l'intersection et la négation); et (ii) nous concevons et étudions un langage fonctionnel d'ordre supérieur qui tire pleinement parti des nouvelles fonctionnalités du système de type. La solution que nous proposons dans cette thèse est générale. Ainsi elle a des domaines d'application autres que les langages pour le traitement de données XML.

Mycoplasma (M.) bovis est une bactérie pathogène des bovins, à l'origine de signes cliniques divers, comme des mammites, des arthrites, des otites et des bronchopneumonies, ces dernières étant majoritaires en France. Les mycoplasmoses à M. bovis ont un fort coût économique et leur contrôle impose une importante mobilisation sanitaire et un recours très fréquent à l'antibiothérapie. Peu de données étaient disponibles jusque récemment concernant le typage moléculaire et l'antibiosensibilité des souches françaises de M. bovis. Deux études antérieures à ce travail et réalisées au sein de l'UMR « Mycoplasmoses des ruminants » ont montré que les isolats cliniques de M. bovis collectés en France après 2000 appartiennent à un sous-type moléculaire majoritaire (ST2), très homogène et sont par ailleurs multirésistants à la plupart des familles antibiotiques à l'exception des fluoroquinolones. Ces résultats suggèrent la diffusion sur le territoire national d'un clone unique multirésistant. Le premier objectif de cette étude était de déterminer les mécanismes à la base de la perte de sensibilité aux antibiotiques des isolats français. Dans un deuxième temps, les liens entre les différents sous-types moléculaires, les profils d'antibiosensibilité, les maladies associées et le polymorphisme des gènes cibles des antibiotiques ont été investigués. Cette approche a été déployée pour trois familles d'antibiotiques utilisées en pratique vétérinaire: les macrolides, les tétracyclines et également les fluoroquinolones, quoique récemment classées comme molécules critiques. De façon générale, les mutations identifiées dans les cibles des antibiotiques expliquent à elles seules les phénotypes de résistance observés. Des mutations dans les ARNs ribosomaux, cibles des macrolides et des tétracyclines, ont été observées sur des isolats cliniques dès 1978 et sont devenues systématiques sur tous les isolats collectés après 2000 et appartenant au sous-type ST2 majoritaire. En ce qui concerne les fluoroquinolones, la faible augmentation des CMI (concentrations minimales inhibitrices) mesurée chez la plupart des isolats cliniques récents n'a pas été associée à des mutations des QRDR (« Quinolones Resistance-Determining Regions »). Par contre, des altérations cumulées de façon séquentielle dans ces QRDR, associées à une hausse des CMI, ont été mises en évidence lors d'expériences de sélection in vitro et majoritairement pour des souches appartenant à un sous-type récent minoritaire, ST3, apparemment plus variable et plus apte à fixer les mutations. En 2013, le premier isolat clinique présentant une CMI augmentée aux fluoroquinolones a été isolé: il appartient à ce sous-type ST3. L'ensemble des résultats obtenus montrent que les différents sous-types de M. bovis n'évoluent pas de la même façon vers la résistance. Ce constat ajouté à celui de la multirésistance des isolats récents (ST2 ou ST3) met en exergue l'intérêt de la surveillance (sous-typage et antibiosensibilité) et le suivi de l'évolution des isolats de M. bovis circulant en France. Ce suivi permettrait notamment d'anticiper une éventuelle émergence de la résistance aux fluoroquinolones / Mycoplasma (M.) bovis is a bacterial pathogen for cattle, responsible for various clinical signs, like mastitis, arthritis, otitis and respiratory diseases, the latter being the main syndrome present in France. Mycoplasmoses have a great economic impact and their control entails drastic sanitary measures and a frequent use of antibiotherapy. Few data was available until recently on the molecular subtyping and the antimicrobial susceptibility of the French strains of M. bovis. Two previous studies done in the UMR « Mycoplasmoses des ruminants » proved that clinical isolates collected in France after the year 2000 belonged to one major subtype (ST2), which is very homogeneous, and that they were multiresistant to the main antimicrobial families except fluoroquinolones. These results suggested the diffusion of one unique multiresistant clone on the national territory. The first aim of the present study was to decipher the molecular mechanisms underlying the loss of susceptibility to antimicrobials of the French strains. Secondly the links between the molecular subtypes, the antibiotics susceptibility profiles, the clinical origins and the polymorphisms of the target genes were assessed. This approach was used for 3 antimicrobial families currently used in veterinary medicine: macrolides, tetracyclines and fluoroquinolones, although recently classified as critical. Actually, the point mutations observed in the target genes of the antimicrobials accounted for the observed resistance phenotypes. Some mutations in the ribosomal RNAs, targets of the macrolides and the tetracyclines, were observed in clinical isolates as soon as 1978 and they were generalized in all isolates collected after 2000 and belonging to the major subtype ST2. Concerning the fluoroquinolones, the slight increase in MIC (Minimum Inhibitory Concentration) observed in most of the recent isolates was not associated with mutations in the QRDR (Quinolone Resistance-Determining Regions). However alterations that were associated with increased MICs were highlighted and proved to be sequentially cumulated during experiments of in vitro selection under antimicrobials pressure. This was mainly true for strains belonging to a recent and uncommon subtype, ST3, which is apparently more variable and more able to fix the mutations. In 2013 the first clinical strain showing an increased MIC to fluoroquinolones was isolated and proved to belong to ST3. The whole results of this study showed that the different subtypes did not evolve with the same speed towards resistance. This fact, associated with the multiresistant phenotype of the recent isolates (ST2 or ST3), highlights the urge to monitor (subtyping and antimicrobial susceptibility profiles) and to follow-up the evolution of the isolates of M. bovis circulating in France in order to anticipate a potential emergence of the resistance to fluoroquinolones

Cette thèse porte sur l'analyse statique de code par typage dans le but de détecter les erreurs dans les programmes avant leur exécution. Plus précisément, nous nous intéressons ici au domaine du sous-typage, dans lequel les propriétés du code sont représentées par des ensemble de contraintes de la forme (t1 <= t2). Nos mécanismes de vérification sont alors basés sur l'agrégation de contraintes de sous-typage et la vérification de leur compatibilité par saturation. Le langage de base sur lequel nous travaillons est un ML étendu, muni de variants et d'un mécanisme de filtrage de motifs. Nous commençons par définir un formalisme nous permettant d'exprimer nos systèmes de types sous forme de règles d'inférences. Ce formalisme présente l'avantage d'être suffisamment souple pour nous permettre de prouver les propriétés de validité et de terminaison de nos systèmes, et suffisamment précis pour nous permettre d'en dériver une implémentation de manière systématique. Après avoir défini un système de types de base pour notre langage, nous en présentons trois extensions originales : * Une amélioration du typage du filtrage de motifs basée en particulier sur l'ajout d'un opérateur de disjonction entre les contraintes de sous-typage. Cet opérateur permet alors d'exprimer, pour chaque cas de filtrage, le lien entre le filtre et les contraintes extraites du typage de l'expression correspondante. Ceci nous permet en particulier de représenter beaucoup plus finement le type de certaines fonctions et ainsi d'accepter plus de programmes valides. * Une alternative au mécanisme classique de généralisation permettant de distinguer les contraintes associées aux différents usages des paramètres des fonctions. Un tel mécanisme rend en particulier la construction de langage "let" de ML obsolète. Mixé avec la première extension, nous obtenons un système permettant d'encoder dans le langage lui même (c'est à dire sans ajouter de construction supplémentaire), un modèle objet intéressant. * Une formalisation des GADT basée sur une implantation originale des variables de type existentielles. En plus d'être compatible avec le sous-typage, cette variante des GADT présente une amélioration notable par rapport aux GADT standards par le fait qu'elle étend les possibilités d'inférence. Les annotations de type, habituellement obligatoires en présence de GADT, deviennent ici presque toutes facultatives. Bien qu'il soit possible de dériver directement une implémentation de ces systèmes, ce qui est principalement utile pour leur compréhension et leur prototypage, les performances des typeurs obtenus de la sorte ne sont pas suffisantes pour analyser des programmes de taille réelle. Ceci est principalement dû aux différentes extensions que nous apportons au langage des contraintes, en particulier les opérateurs de disjonction et de négation. Nous présentons alors les différentes techniques que nous avons mises en place pour l'implémentation de nos systèmes permettant à nos analyses de passer à l'échelle en pratique. / This PHD thesis focuses on static analysis of programs by type inference in order to detect program errors before their execution. More precisely, we focus hear in the field of sub-typing, where program properties are described by sets of constraints of the form (t1 <= t2). Our verification mechanisms are based on the aggregation of sub-typing constraints and checking of their compatibility by saturation. The base language on which we define our type systems is an ML-like language provided with variants and pattern matching. We starts by defining a formalism to express our type systems thanks to inference rules. This formalism has the advantage to be sufficiently flexible to allow proving validity and termination properties of our systems, and sufficiently precise to allow a systematic derivation of our inference rules into a runnable typer. After the definition of a base type system for our language, we present three novel extensions: * An improvement of type inference for the pattern matching based on the addition of the "or" operator between sub-typing constraints. This operator allow to express a link, in each cases of a match, between the pattern and the constraints generated at typing time of the case expression. This allows us to refine the type of some functions, and then to accept more valid programs. * A new implementation of the generalization mechanism. This allows to distinguish constraints associated to the different occurrences of a function parameter in its body. Thanks to this mechanism, the "let" construction from ML is in particular obsolete. By mixing this extension with the first one, we obtain a type system able to encode "objects" without any additional language construction. * A formalization of GADT based on an novel implementation of existential type variables. In addition to be compatible with the sub-typing context of this thesis, this alternative to GADT has the advantage to improve type inference. As a consequence, most of type annotations, usually required in the presence of GADT, are now optional. Despite the fact that it is possible to directly derive an implementation of our type systems from their rules, that is principally interesting for their comprehension and prototyping, the effectiveness of such typer is insufficient to analyze real world programs. This is principally due to the extensions we provide to the language of constraints, and in particular to the "or" and "not" operators. At then end, we present multiple techniques we used in our implementation to extend the scalability of our analysis.

Les toxines botuliques (BoNTs) sont les substances les plus toxiques connues. Elles sont responsables du botulisme, une maladie rare mais le plus souvent mortelle sans prise en charge médicale. Cependant, les applications médicales des BoNTs sont de plus en plus nombreuses du fait de leurs propriétés paralysantes. Leur toxicité par voie inhalée en fait un des 6 principaux agents du risque intentionnel. Les BoNTs, produites par Clostridium botulinum, se répartissent en 7 types sérologiques qui se déclinent en sous-types. Cette biodiversité rend difficile leur identification par les méthodes classiques utilisées pour les toxines protéiques (approches immunologiques). Jusqu’à présent, seule l’analyse génétique permettait de distinguer les différents sous-types entre eux. Dans ce travail a été développée une méthode d’analyse en LC-QqQ-MS/MS en mode MRM pour identifier les différents sous-types de la BoNT/A dans des matrices complexes à partir de peptides communs et spécifiques à ces sous-types. Un traitement d’échantillon par immunocapture sur billes magnétiques couplées à des anticorps anti-peptides a été développé pour isoler la toxine de l’échantillon avant analyse. Des surnageants de culture des sous-types A1 à A3, A5, A7 à A8 ont été utilisés pour valider la méthode. La limite de détection de la méthode est compatible avec les taux de toxine retrouvés habituellement dans les échantillons naturellement contaminés. Cette méthode de spectrométrie de masse a ensuite été utilisée pour quantifier les différents sous-types de la BoNT/A dans une matrice complexe (surnageants de culture de C. botulinum). Une technique de quantification, utilisant un isotope stable de la chaine légère de type A1, ([13C6]K et [13C6]R), a été retenu comme étalon interne. Les différents sous-types de BoNT/A ont été quantifiés dans les surnageants et la quantité de BoNT correspondante à une dose létale minimale de 100% a été déterminée pour chaque sous-type. / Botulinum neurotoxins (BoNTs) are the most poisonous substances known. They are responsible for human botulism, a rare but potentially fatal disease if not quickly treated. However, BoNTs were approved for the treatment of numerous medical applications due to their temporary paralysis effects. BoNTs are among the six agents with the highest risk of potential use as bio-weapons because of their high toxicity in aerosol form. BoNTs, produced by Clostridium botulinum, are divised into seven toxinotypes and each toxinotype contains several subtypes. This biodiversity makes more difficult their identification with classical methods by immunological ways. Until now, only molecular genetical methods could differenciate subtypes among them. The aim of this work was to develop a liquid chromatography tandem mass spectrometry (LC-MS/MS) in MRM mode to efficiently discrimate the distinct subtypes from specific and common peptides. Immunocapture sample preparation with antipeptides antibodies was used and allowed the isolation of the toxin from the sample. Subtyping was performed with crude supernatants (BoNT/A1 to /A3, /A5, /A7 and /A8) in order to validate the method. Limit of detection (LOD) of the proposed method is in the range of minimal toxin concentration found in naturally contamined samples. In a second part of this work, this mass spectrometry method was used to quantify the neurotoxin in complex matrices (supernatants of Clostridium botulinum cultures). Isotope labeled light chain (13C6]K et [13C6]R) from botulinum A1 neurotoxin was produced and used as internal standart. Subtypes were quantified in supernatants and the quantity of neurotoxin for one minimal lethal dose 100% was determined for each subtype