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

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.

Mycobacterium bovis, agent étiologique de la tuberculose bovine (bTB), affecte principalement les bovins mais évolue également dans des systèmes multi-hôtes. La France possède le statut UE indemne de bTB depuis 2000, mais la prévalence de la maladie a augmenté régulièrement ces cinq dernières années. Son contrôle passe par la connaissance des nouveaux facteurs de risque. Pour les déceler, nous avons étudié l’évolution spatio-temporelle de la bTB via la caractérisation des souches isolées de foyers français depuis 1978. A partir de plus de 2.000 souches, environ 600 profils génétiques ont été définis par spoligotypage et typage MLVA. Les groupes majoritairement identifiés, SB0120, SB0134, SB0121 et la «famille F4», sont différenciés plus finement par le MLVA qui augmente la puissance des études d’épidémiologie moléculaire. La diminution de la variabilité génétique et des changements de la distribution géographique des souches s’explique par des modifications dans les pratiques d’élevages et par la prolifération de certains génotypes évoluant dans des systèmes multi-hôtes. L’identification des groupes clonaux existants en France est confirmée par l’étude de mutations SNP effectuée suite au séquençage total de 82 génomes sélectionnés. De nouveaux outils de typage visant à affiner l’identification des souches, définir des profils de transmission méconnus et établir des liens épidémiologiques entre animaux sauvages et de rente sont envisagés. / Myobacterium bovis is the causative agent of bovine tuberculosis (bTB), principally affecting cattle but also evolving in multi-host livestock-wildlife systems. Prevalence is regularly increasing in France, an EU bTB-free state since 2000’s, after a 50 year collective fighting-campaign. To control the disease, it is necessary to acknowledge new risk factors. For identifying them, we have studied the spatial-temporary evolution of the disease by characterizing M. bovis strains causative of French outbreaks since 1978. Within more than 2,000 strains, around 600 profiles could be defined by spoligotyping and MLVA. SB0120, SB0134, SB0121 and the « F4 family » are the major spoligotypes isolated. In these groups, the refinement of differentiation can be increased by MLVA typing for powerful molecular epidemiological studies. Decreases in genetically and geographical variability could be explained by changes in husbandry practices and by the proliferation of unique genotypes in multi-host systems. Identification of clonal groups coexisting in France is confirmed by the study of SNPs mutations deduced from the whole genome sequencing of 82 representative strains. New typing tools for refining strains identification and disclosing unknown transmission patterns between livestock and wildlife are foreseeable

Les entérovirus (EV) humains, membres de la famille des Picornaviridae, comprennent plus de 100 génotypes appartenant à 4 espèces : Enterovirus A, B, C et D. Ces virus sont à l’origine de pathologies très variées et occupent une place importante en santé publique. La méthode conventionnelle de typage des EV consiste en une réaction de séroneutralisation avec des antisérums spécifiques à partir de souches isolées en culture cellulaire ; cette technique est longue, coûteuse et limitée par sa capacité à identifier correctement les variants antigéniques et les nouveaux génotypes. De plus, elle est limitée aux génotypes cultivables. De nouvelles méthodologies de typage moléculaire par séquençage partiel du génome ont été récemment développées ; elles consistent à analyser une partie variable de la région codant une des protéines de capside (VP1 ou alternativement VP2 ou VP4). Cependant ces techniques sont le plus souvent réalisées à partir de souches isolées en culture cellulaire. Le but de ce travail a été de développer une technique de typage des EV directement sur des prélèvements cliniques en se basant sur le séquençage partiel de la région VP2 dont le laboratoire avait montré précédemment l’intérêt (Nasri et al., 2007). Pour le dessin des amorces, nous avons utilisé la stratégie CODEHOP (COnsensus DEgenerate Hybrid Oligonucleotide Primer) de manière à améliorer à la fois la spécificité et la sensibilité de la méthode d’amplification. Nous présentons ici un premier article décrivant la nouvelle technique de typage VP2 et rapportons son application au typage d’échantillons cliniques trouvés positifs par une PCR ciblant la région 5’ non codante du génome des EV sur une période de trois ans. Le deuxième article présente pour la première fois l’application d’une technique de typage direct à des échantillons environnementaux d’eaux usées. Le troisième article montre l’intérêt de coupler deux techniques de typage ciblant des régions différentes (VP1 et VP2) pour l’identification de souches d’EV isolées par culture cellulaire en Centre-Afrique. Malgré des problèmes de sensibilité, cette nouvelle technique de typage directement à partir d’échantillons peut rendre de grands services tant en clinique humaine que pour la surveillance environnementale / Human enteroviruses (EV), members of the Picornaviridae family, comprise more than 100 genotypes belonging to four species: Enterovirus A, B, C and D. These viruses are responsible for a wide range of pathologies and play an important role in Public Health. The classic method for typing EVs consists in a seroneutralisation assay with specific antisera using strains isolated by cell culture; this technique is cumbersome, expensive and unable to type currently antigenic variants and new serotypes. In addition, it is limitated to culturable serotypes. New methods of molecular typing by partial sequencing of the genome have been recently developed; they consist in analysing a variable part of the region coding for capsid protein (VP1 or alternatively VP2 or VP4). However, these techniques are usually performed on strains isolated by cell culture. The aim of this work was to develop a typing method able to work from clinical specimens by partial sequencing of the VP2 region, which had been shown to exhibit a good typing performance (Nasri et al., 2007). For the design of primers, we used the CODEHOP (COnsensus DEgenerate Hybrid Oligonucleotide Primer) strategy on order to improve the sensitivity and the specificity of the amplification assay. We present herein a first article that describes in details the new VP2 typing method and requests its use for typing clinical specimens found positive by a PCR assay targeting the 5’ non coding region of EVs over a period of three years. The second paper describes for the first time the direct use of a typing method on environtmental wastewater samples. The third article shows the interest of coupling 2 typing techniques targeting different regions (VP1 and VP2) of the EV genome for the identification of strains isolated by cell culture in Republic of Central Africa. Despite a loss of sensitivity, the new VP2 typing method used directly on specimens was found to be of great help both for human diagnosis and environmental surveillance

La spectrométrie de masse de type MALDI-TOF vient d'être largement adoptée dans les laboratoires de microbiologie clinique, qu'ils soient de ville ou hospitalier. Le MALDI-TOF est maintenant utilisée en routine pour l'identification des micro-organismes. Les micro-organismes sont identifiés en quelques minutes à un coût minime et avec une meilleure précision qu'en utilisant les méthodes conventionnelles. Le MALDI-TOF permet une identification microbienne révolutionnaire mais il ne permet pas aisément la détection de résistances aux antimicrobiens ou de facteurs de virulence. Le travail de thèse a eu pour objectif d'adresser cette problématique : est-il possible d'identifier, de typer un micro-organisme et de détecter sa résistance ou sa virulence par spectrométrie de masse ? Pour cela, l'utilisation d'une chromatographie liquide conventionnelle couplée à un spectromètre de type triple-quadripôle travaillant en mode SRM a été proposée. Nous avons démontré que la caractérisation complète des micro-organismes était possible à l'aide d'une seule méthode. La preuve de concept a été apportée pour des bactéries à Gram positive, à Gram négative et pour des levures. L'approche a été démontrée pour la détection des mécanismes majeurs de résistance aux bêta-lactamines, aux glycopeptides et aux azolés. La détection de toxines a également été démontrée. Fort de ces démonstrations, une évaluation clinique a été réalisée avec des souches et des hémocultures cliniques. La caractérisation de staphylocoques dorés, une des espèces capitales dans les maladies infectieuses du fait de sa prévalence, de sa sévérité et de sa résistance aux antibiotiques, a été engagée pour illustrer l'intégration de l'approche ESI-MS. La méthode SRM développée a permis en moins de deux heures d'obtenir des résultats en parfait accord avec les méthodes conventionnelles. Ce concept ouvre de nouveaux horizons pour la spectrométrie de masse en microbiologie clinique / Whole cell mass spectrometry based on MALDI-TOF technology has been broadly embraced in clinical microbiology. MALDI-TOF is routinely used for microbial identification. WC-MS is faster, more accurate and cheaper for large laboratories than conventional biochemical tests. MALDI-TOF revolutionizes microbial identification but the selection of the right antibiotic treatment still requires time consuming antibiotic susceptibility testing. Thesis work is dedicated to answer to this problematic : it is possible to perform identification of a micro-organism to the species or sub-species level and to detect its resistance or its virulence by mass spectrometry ? To this purpose, a conventional bore chromatography coupled to a triple-quadripole mass spectrometer in SRM mode is proposed. We show that complete microorganism characterization was possible thanks to only one method. A proof of concept was given for Gram negative, for Gram positive and for yeasts. The approach was extended to major resistance mechanisms to beta-lactamin, to glycopeptides and to azoles. Toxins detection was also proved. Driven by this success, a clinical evaluation was carried out based on strains and blood culture. Staphylococcus aureus was chosen to illustrate ESI-MS approach integration. This common Gram positive commensal bacteria is responsible for both community- and hospital-acquired infections. The developed SRM method allows obtaining results in less than two hours in perfect agreement with conventional methods. This concept opens new horizons for mass spectrometry in clinical microbiology

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

La sécurité alimentaire est basée sur des systèmes de cultures durables. Les agents phytopathogènes présentent un risque sérieux pour la stabilité de l'agriculture mondiale. Dans ce contexte, la biosurveillance des agents phytopathogènes s'avère indispensable afin de connaitre et de comprendre la répartition, les routes et les facteurs de dispersion des populations phytopathogènes, et de prendre les mesures adaptées pour limiter leur propagation. Le genre bactérien Xanthomonas comprend un ensemble d'espèces phytopathogènes-spécifiques s'attaquant a une large gamme d'espèces végétales dont certaines sont importantes pour la production agricole. Les deux espèces d'étude, i.e les pathovars de Xanthomonas oryzae (Xo) et Xanthomonas axonopodis pathovar manihotis (Xam), pathogènes respectivement du riz et du manioc, font partie du « top 10 » des bactéries phytopathogènes d'importance majeure dans le monde. Des travaux portant sur l''épidémiosurveillance de ces bactéries phytopathogenes doivent pouvoir être mis en place en routine. L'objectif est de typer et de relier ces souches bactériennes à différentes échelles géographiques, ainsi que de détecter et caractériser les épidémies de manière précoce. Pour ce faire, plusieurs approches de typage moléculaire à haut niveau de résolution ont été explorées. Des marqueurs moléculaires basés sur les loci VNTR (Variable Number of Tandem repeats) ont été étudiés. Chez X. oryzae, un outil MLVA-25 (Multilocus VNTR Analysis) pour le pathovar Xanthomonas oryzae pv. oryzicola (Xoc) et un outil MLVA-16 pour les trois lignées génétiques de X. oryzae ont été développés. L'étude par le MLVA-16 de populations de X. oryzae a permis de caractériser des complexes clonaux généralement associés à de nouvelles épidémies. La description de nouvelles souches de Xoc en Afrique Centrale et Afrique de l'Est indique une provenance vraisemblablement d'origine asiatique. Chez Xam, la recherche de loci VNTR polymorphiques sur 65 génomes de Xam complets a abouti à la description de seize loci VNTR robustes donc cinq ont été ensuite utilisés pour l'étude de populations de Xam dans les plaines de l'est Colombien. Cette dernière étude met en avant une structuration des populations de Xam selon les régions. Enfin, une méthode de spoligotypage associée aux locus CRISPR-Cas (Clustered Regularly Interspaced Short Palindromic Repeats) et des marqueurs minisatellites ont été développés chez les souches du pathovar Xanthomonas oryzae pv. oryzae (Xoo). Les analyses préliminaires ont permis de définir la composition de la cassette CRISPR et de proposer des outils de spoligotypage utiles pour les souches asiatiques de Xoo. D'autre part, 18 marqueurs minisatellites ont indiqué une corrélation significative avec les races des souches et peuvent servir à l'étude plus large de populations Xoo philippines ou asiatiques. En conclusion, des nouvelles approches de typage moléculaire ont été évaluées, mises au point et employées avec succès pour étudier les bactéries pathogènes du riz et du manioc appartenant au genre Xanthomonas. / Food and agriculture safety rely on durable cropping systems. Consequently, phytopathogens pose a serious risk for durable agriculture in the world. In this context, surveillance of phytopathogens is a mandatory prerequisite in order to understand and to predict pathogen repartition, dispersion routes and factors, and to trigger appropriate measures to reduce the pathogen's propagation. The genus Xanthomonas displays a large diversity of host-specific plant-pathogenic species that infect a wide range of plant species, including commercially grown crops. The two studied species, i.e. the rice-pathogenic Xanthomonas oryzae and the cassava-pathogenic Xanthomonas axonopodis pathovar manihotis (Xam), belong to the top-10 of phytopathogenic bacteria and are thus of major interest. Routine epidemiological surveillance of these bacteria has to be achieved in order to type and link strains at different geographic scales as well as to characterize outbreaks and epidemics. For this purpose, several high-resolution molecular typing approaches were explored. Firstly, VNTR (Variable Number of Tandem repeats)-based molecular markers were studied. For X. oryzae, multilocus VNTR analyses (MLVA) were developed: MLVA-25 for the pathovar oryzicola (Xoc) and MLVA- 16 for the three known lineages of X. oryzae. A large population study of X. oryzae by MLVA-16 allowed us to characterize genetic clonal complexes, which were likely associated with new epidemics. Also, the novel description of Xoc strains from central and east Africa indicated their probable Asian provenance. For Xam, the exploration of polymorphic VNTR loci in 65 available genome sequences allowed the description of sixteen robust VNTR loci. Among them, five highly polymorphic loci were further used in a population study of Xam in the eastern plain of Colombia. The results provided evidence of a geographical Xam population structuration. Secondly, CRISPR (Clustered Regularly Interspaced Short Palindromic Repeats)-associated spoligotyping and minisatellites markers were explored for a largely divergent set of Philippine strains of Xanthomonas oryzae pv. oryzae (Xoo). Both approaches were compared to genome-wide SNPs and races. Preliminary studies identified the composition of CRISPR arrays, which could be useful for a spoligotyping approach. On the other hand, 18 minisatellites markers revealed a significant correlation with races and could be used for a larger study of Philippine or Asian Xoo populations. In conclusion, novel molecular typing approaches were successfully evaluated, implemented and used to study rice- and cassava-pathogenic bacteria of the genus Xanthomonas.

Cette thèse porte sur l'étude de différents aspects de la sécurité des protocoles de vote électronique à distance. Ces protocoles décrivent comment organiser des élections par Internet de manière sécurisée. Ils ont notamment pour but d'apporter des garanties de secret du vote, et de vérifiabilité - ie, il doit être possible de s'assurer que les votes sont correctement comptabilisés. Nos contributions portent sur deux aspects principaux. Premièrement, nous proposons une nouvelle technique d'analyse automatique de propriétés d'équivalence, dans le modèle symbolique. De nombreuses propriétés en lien avec la vie privée s'expriment comme des propriétés d'équivalence, telles que le secret du vote en particulier, mais aussi l'anonymat ou la non-traçabilité. Notre approche repose sur le typage: nous mettons au point un système de typage qui permet d'analyser deux protocoles pour prouver leur équivalence. Nous montrons que notre système de typage est correct, c'est-à-dire qu'il implique effectivement l'équivalence de traces, à la fois pour des nombres bornés et non bornés de sessions. Nous comparons l'implémentation d'un prototype de notre système avec les autres outils existants pour l'équivalence symbolique, sur divers protocoles de la littérature. Cette étude de cas montre que notre procédure est bien plus efficace que la plupart des autres outils - au prix d'une perte de précision (notre outil peut parfois échouer à prouver certaines équivalences). Notre seconde contribution est une étude des définitions du secret du vote et de la vérifiabilité - ou, plus précisément, la vérifiabilité individuelle, une propriété qui requiert que chaque votant soit en mesure de vérifier que son propre vote a bien été pris en compte. Nous prouvons, aussi bien dans les modèles symboliques que calculatoire, que le secret du vote implique la vérifiabilité individuelle, alors même que l'intuition et des résultats voisins déjà établis semblaient indiquer que ces deux propriétés s'opposent. Notre étude met également en évidence une limitation des définitions existantes du secret du vote par jeux cryptographiques : elles supposent une urne honnête, et par conséquent expriment des garanties significativement plus faibles que celles que les protocoles visent à assurer. Nous proposons donc une nouvelle définition (par jeu) du secret du vote, contre une urne malhonnête. Nous relions notre définition à une notion de secret du vote par simulation, pour montrer qu'elle apporte des garanties fortes. Enfin, nous menons une étude de cas sur plusieurs systèmes de vote existants. / In this thesis we study several aspects of the security of remote electronic voting protocols. Such protocols describe how to securely organise elections over the Internet. They notably aim to guarantee vote privacy - ie, votes must remain secret -and verifiability - it must be possible to check that votes are correctly counted. Our contributions are on two aspects. First, we propose a new approach to automatically prove equivalence properties in the symbolic model. Many privacy properties can be expressed as equivalence properties, such as in particular vote privacy, but also anonymity or unlinkability. Our approach relies on typing: we design a type system that can typecheck two protocols to prove their equivalence. We show that our type system %, together with some additional conditions on the messages exchanged by the protocols, soundly implies trace equivalence, both for bounded and unbounded numbers of sessions. We compare a prototype implementation of our typechecker with other existing tools for symbolic equivalence, on a variety of protocols from the literature. This case study shows that our procedure is much more efficient than most other tools - at the price of losing precision (our tool may fail to prove some equivalences). Our second contribution is a study of the definitions of privacy and verifiability - more precisely, individual verifiability, a property that requires each voter to be able to check that their own vote is counted. We prove that, both in symbolic and computational models, privacy implies individual verifiability, contrary to intuition and related previous results that seem to indicate that these two properties are opposed. Our study also highlights a limitation of existing game-based definitions of privacy: they assume the ballot box is trusted, which makes for significantly weaker guarantees than what protocols aim for. Hence we propose a new game-based definition for vote privacy against a dishonest ballot box. We relate our definition to a simulation-based notion of privacy, to show that it provides meaningful guarantees, and conduct a case study on several voting schemes.

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.

L’objectif de cette étude est de déterminer l’importance clinique de l’antigène érythrocytaire canin Dal, en investiguant sa prévalence, son mode d’héritabilité et son immunogénicité. Un total de 1230 chiens a été recruté à travers l’Amérique du Nord et typés pour le Dal en utilisant des allo-anticorps polyclonaux et une technique sur colonne de gel. Des individus Dal-négatifs ont été identifiés chez les Dalmatiens (n=15/128), Doberman Pinschers (n=183/432), Shih Tzus (n=12/21), chiens de races croisées (3/122), Beagles (2/100), Lhasa Apso (1/3) et Bichon Frisé (1/6). Six donneurs de sang Dal-négatifs ont été identifiés, dont 5 Doberman Pinschers (1/228 donneurs d’une autre race). Tous les autres chiens testés étaient Dal-positifs (n=418). La rareté du sang Dal-négatif place les chiens Dal-négatifs à risque d’incompatibilité transfusionnelle lors de transfusions multiples. Cette étude est la première à identifier des individus Dal-négatifs chez des chiens de race autre que Dalmatien et à établir le mode d’héritabilité du Dal, soit autosomal dominant. Par la suite, 2 Beagles Dal-négatifs ont été sensibilisés spécifiquement pour le Dal en recevant une transfusion Dal-positif. Suivant la sensibilisation, des allo-anticorps anti-Dal ont été détectés à partir du 4ième jour post-transfusion et sont demeurés détectables jusqu’à 2 ans post-transfusion. Les titres d’agglutination maximaux (1:64 et 1:1024) ont été atteints 2 et 1 mois post-transfusion chez le chien #1 et le chien #2, respectivement. Cette étude a confirmé l’immunogénicité du Dal tout en ayant généré une quantité considérable d’allo-anticorps anti-Dal permettant de futurs typages sanguins Dal. / The purpose of this study was to determine the clinical importance of the Dal canine erythrocyte antigen by investigating its prevalence, its mode of inheritance and its immunogenicity. A total of 1230 dogs recruited from North America were blood typed for Dal applying a gel column technique using polyclonal canine anti-Dal sera. Dal-negative dogs were identified mostly in Dalmatians (15/128), Dobermans Pinschers (183/432) and Shih Tzus (12/21), and sporadically in mixed breed dogs (3/122), Beagles (2/100), Lhasa Apso (1/6) and Bichon Frise (1/3). All other dogs tested were Dal-positive (n= 418). Six Dal-negative blood donors were found, including 5 Doberman Pinschers (1/228 non-Dalmatian and non-Doberman Pinscher blood donors). The scarcity of Dal-negative blood donors puts Dal-negative patient at higher risk of transfusion incompatibility if requiring multiple blood transfusions. This study was the first to identify Dal-negative dogs in other breeds than Dalmatians and to establish an autosomal dominant mode of inheritance of the Dal-positive phenotype. Secondly, 2 Dal-negative healthy research Beagles were sensitized specifically for Dal with a Dal-positive packed red blood cell transfusion. Following sensitization, anti-Dal alloantibodies were detected as early as 4 days post-transfusion and remained detectable 2 years post-transfusion, with maximum agglutination titers (1:1024 and 1:64) reached respectively 1 and 2 months posttransfusion in dog #2 and dog #1. Our study confirmed the immunogenicity of the Dal and allowed banking of a considerable amount of polyclonal antisera for further Dal blood typing.