Les revues systématiques sont des outils indispensables à la synthèse des connaissances en évaluation thérapeutique. Il est désormais fréquent que plusieurs traitements soient disponibles pour une même indication. L’objectif des patients et des cliniciens est alors de savoir quels sont, parmi l’ensemble des traitements disponibles, le(s) meilleur(s). Compte tenu de la nécessité de synthétiser les données disponibles pour tous les traitements et de maintenir cette synthèse à jour, notre objectif était d’évaluer les limites du système actuel de synthèse et de développer une méthodologie alternative. Nous avons d’abord évalué la capacité des revues systématiques à prendre en compte l’ensemble des preuves disponibles sur l’effet des multiples traitements. Nous avons utilisé l’exemple des traitements de deuxième ligne du cancer bronchique non à petites cellules métastatique non muté pour EGFR ou de statut inconnu. Nous avons montré que les 29 revues systématiques publiées jusque 2015 sur cette question, considérées collectivement, fournissaient une synthèse fragmentée et non à jour de la preuve disponible. Au moins 40% des 77 essais, des 45 traitements, des 54 comparaisons de traitements et des 28 636 patients n’étaient constamment pas pris en compte dans les revues systématiques. Nous avons discuté les raisons pour lesquelles le système de synthèse des données actuel ne permettait pas de couvrir l’ensemble des données disponibles. Nous avons ensuite développé une nouvelle forme de synthèse de la preuve disponible au cours du temps, la méta-analyse en réseau cumulative et dynamique. Elle consiste à passer d’une série de méta-analyses à une méta-analyse en réseau unique, incluant l’ensemble des traitements disponibles pour une indication donnée, avec une mise à jour du réseau d’essais et de la synthèse des données dès que les résultats d’un nouvel essai deviennent disponibles. Elle débute par une méta-analyse en réseau initiale suivie d’une succession de mises à jour répétées à intervalles réguliers. Nous avons décrit les étapes méthodologiques, et développé le protocole d’une étude de preuve de concept, appliquée aux traitements de deuxième ligne du cancer bronchique non à petites cellules. Enfin, nous avons réalisé la méta-analyse en réseau initiale sur ce même exemple. Nous avons inclus 98 essais randomisés évaluant 60 traitements chez 34 179 patients. Nous avons montré que les traitements par immunothérapie (nivolumab et pembrolizumab) avaient un effet sur la survie globale supérieur aux chimiothérapies et thérapeutiques ciblées actuellement recommandées (nivolumab versus docetaxel HR=0,68 (IC95% 0,55-0,83) ; versus pemetrexed HR=0,65 (0,5-0,83) ; versus erlotinib HR=0,66 (0,51-0,84) and versus gefitinib HR=0,65 (0,51-0,82)). Les résultats étaient similaires pour le pembrolizumab. Pour la survie sans progression, le nivolumab avait aussi un effet supérieur aux quatre traitements recommandés. La méta-analyse en réseau cumulative et dynamique pourrait devenir l’outil permettant de changer de paradigme dans la synthèse des connaissances afin d’améliorer la prise de décision médicale. / Systematic reviews are essential tools to synthesize available evidence for therapeutic evaluation. Multiple treatments are now frequently available for a given condition. Patients and physicians want to know which one is the best among all treatments. Thus we need to retrieve and synthesize all available evidence across all treatments and furthermore to maintain it updated when new evidence and new treatments become available. Our objective was to evaluate the limits of the current ecosystem of evidence synthesis and to develop an alternative methodology. We have first assessed the capacity of systematic reviews to cover all available evidence of multiple treatments. We took the example of second-line treatments of advanced non-small cell lung cancer with EGFR wild-type or unknown status. We have shown that the 29 systematic reviews published in this condition up to 2015, considered collectively, failed to provide a complete and updated synthesis of all available evidence. Almost 40% of the 77 trials, of the 45 treatments, of the 54 treatment comparisons and of the 28,636 patients were always missing from systematic reviews. We have discussed the reasons why the ecosystem of evidence synthesis fails to encompass all available evidence. We then developed a new paradigm to synthesize evidence over time called live cumulative network meta-analysis. This new concept consists in switching from a series of standard meta-analyses to a single network meta-analysis covering all treatments and systematically updated as soon as the results of a new trial become available. Live cumulative network meta-analysis is initiated with a network meta-analysis which is iteratively updated. We have described the methodological steps, developed the protocol of a proof-of-concept study applied to second-line treatments of advanced non-small cell lung cancer. Finally, we have performed the initial network meta-analysis in this condition. We have included 98 trials including 34,179 patients and assessing 60 treatments. We have shown that nivolumab was more effective in term of overall survival compared to docetaxel HR=0.68 (IC95% 0.55-0.83), to pemetrexed HR=0.65 (0.5-0.83), to erlotinib HR=0.66 (0.51-0.84) and to gefitinib HR=0.65 (0.51-0.82). Similar results were found with pembrolizumab. In progression free survival, nivolumab had a more important treatment effect compared to the four recommended treatments. Live cumulative network meta-analysis should become a paradigmatic shift for systematic reviews and meta-analysis in order to improve medical decision making.

Cette thèse présente une formalisation en Coq des langages et des algorithmes fondamentaux portant sur les bases de données. Ainsi, ce fourni des spécifications formelles issues des deux approches différentes pour la définition des modèles de données: une basée sur l’algèbre et l'autre basée sur la logique.A ce titre, une première contribution de cette thèse est le développement d'une bibliothèque Coq pour le modèle relationnel. Cette bibliothèque contient les modélisations de l’algèbre relationnelle et des requêtes conjonctives. Il contient aussi une mécanisation des contraintes d'intégrité et de leurs procédures d'inférence. Nous modélisons deux types de contraintes: les dépendances, qui sont parmi les plus courantes: les dépendances fonctionnelles et les dépendances multivaluées, ainsi que leurs axiomatisations correspondantes. Nous prouvons formellement la correction de leurs algorithmes d'inférence et, pour le cas de dépendances fonctionnelles, aussi la complétude.Ces types de dépendances sont des instances de contraintes plus générales : les dépendances génératrices d'égalité (equality generating dependencies, EGD) et, respectivement, les dépendances génératrices de tuples (tuple generating dependencies, TGD), qui appartiennent a une classe encore plus large des dépendances générales (general dependencies). Nous modélisons ces dernières et leur procédure d'inférence, i.e, "the chase", pour lequel nous établissons la correction. Enfin, on prouve formellement les théorèmes principaux des bases de données, c'est-à-dire, les équivalences algébriques, la théorème de l' homomorphisme et la minimisation des requêtes conjonctives.Une deuxième contribution consiste dans le développement d'une bibliothèque Coq/ssreflect pour la programmation logique, restreinte au cas du Datalog. Dans le cadre de ce travail, nous donnons la première mécanisations d'un moteur Datalog standard et de son extension avec la négation. La bibliothèque comprend une formalisation de leur sémantique en theorie des modelés ainsi que de leur sémantique par point fixe, implémentée par une procédure d'évaluation stratifiée. La bibliothèque est complétée par les preuves de correction, de terminaison et de complétude correspondantes. Cette plateforme ouvre la voie a la certification d' applications centrées données. / This thesis presents a formalization of fundamental database theories and algorithms. This furthers the maturing state of the art in formal specification development in the database field, with contributions stemming from two foundational approches to database models: relational and logic based.As such, a first contribution is a Coq library for the relational model. This contains a mechanization of integrity constraints and of their inference procedures. We model two of the most common dependencies, namely functional and multivalued, together with their corresponding axiomatizations. We prove soundness of their inference algorithms and, for the case of functional ones, also completeness. These types of dependencies are instances of equality and, respectively, tuple generating dependencies, which fall under the yet wider class of general dependencies. We model these and their inference procedure,i.e, the chase, for which we establish soundness.A second contribution consists of a Coq/Ssreflect library for logic programming in the Datalog setting. As part of this work, we give (one of the) first mechanizations of the standard Datalog language and of its extension with negation. The library includes a formalization of their model theoretical semantics and of their fixpoint semantics, implemented through bottom-up and, respectively, through stratified evaluation procedures. This is complete with the corresponding soundness, termination and completeness proofs. In this context, we also construct a preliminary framework for dealing with stratified programs. This work paves the way towards the certification of data-centric applications.

Le traitement de la leucémie myéloïde chronique (LMC) par imatinib est un succès de thérapie ciblée en oncologie. Le principe de cette thérapie est de bloquer les processus biochimiques à l'origine du développement de la maladie, et de permettre à une majorité de patients de réduire leurs risques de progression mais aussi d'éviter des traitements lourds et risqués comme la greffe de cellules souches hématopoïétiques.Cependant, même si l'efficacité de l'imatinib à été prouvée dans un contexte clinique, il n'en demeure pas moins qu'une proportion non négligeable de patients n'obtient par de niveaux de réponse moléculaire jugés optimale. Le but de cette thèse est de tester l'hypothèse d'un lien entre des polymorphismes de gènes impliqués dans l'absorption des médicaments et de leurs métabolisme, et la réponse moléculaire dans la leucémie myéloïde chronique en phase chronique traitée par imatinib.Dans le but d'évaluer la réponse moléculaire des patients, des prélèvements sanguins sont réalisés tout les 3 mois afin de pratiquer le dosage d'un biomarqueur. Ce type particulier de suivi produit des données censurées par intervalles. Comme par ailleurs, les patients demeurent à risque de progression ou sont susceptible d'interrompre leurs traitements pour cause d'intolérance, il est possible que la réponse d'intérêt ne soit plus observable sous le traitement étudié. Les données ainsi produites sont censurées par intervalles dans un contexte de compétition (risques compétitifs).Afin de tenir compte de la nature particulière des données collectées, une méthode basée sur l'imputation multiple est proposée. L'idée est de transformer les données censurées par intervalles en de multiples jeux de données potentiellement censurées à droite et d'utiliser les méthodes disponibles pour l'analyser de ces données. Finalement les résultats sont assemblés en suivant les règles de l'imputation multiple. / Imatinib in the treatment of chronic myeloid leukemia is a success of targeted therapy in oncology. The aim of this therapy is to block the biochemical processes leading to disease development. This strategy results in a reduction of the risk of disease progression and allows patients to avoid extensive and hazardous treatments such as hematologic stem cell transplantation.However, even if imatinib efficacy has been demonstrated in a clinical setting, a significant part of patients do not achieve suitable levels of molecular response. The objective of this thesis, is to test the hypothesis of a correlation between polymorphisms of genes implied in drug absorption an metabolism and the molecular response in chronic myeloid leukemia in chronic phase treated by imatinib.In order to evaluate patients molecular response, blood biomarker assessments are performed every 3 months. This type of follow up produces interval censored data. As patients remain at risk of disease progression, or may interrupt their treatments due to poor tolerance, the response of interest may not be observable in a given setting. This situation produces interval censored competing risks data.To properly handle such data, we propose a multiple imputation based method.The main idea is to convert interval censored data into multiple sets of potentially right censored data that are then analysed using multiple imputation rules.

La force particulière attribuée à l'aveu judiciaire civil procède, à l'origine, d'un rattachement contestable à la confessio in jure, qui constituait un acquiescement à la demande. Si l'on restitue à l'aveu sa dimension probatoire qu'avait dégagée le droit savant médiéval, il apparaît que la nature de l'aveu porte l'empreinte de la volonté alors que son régime est fortement influencé par la recherche d'une vérité par le juge. D'un côté, l'exigence d'intégrité et de liberté de la volonté d'avouer, en droit judiciaire privé comme en procédure pénale, donne à l'aveu la nature d'un acte juridique destiné à constituer une preuve, laquelle ne peut porter que sur un fait. Il est alors possible de distinguer les véritables aveux, qui procèdent d'une telle volonté, d'autres figures juridiques dans lesquelles l'aveu est retenu à titre de sanction contre le plaideur qui, en procédure civile ou en contentieux administratif, méconnaît l'imperium procédural du juge. De l'autre côté, la preuve constituée par l'aveu est toujours appréciée souverainement par les juges du fond. Si le juge judiciaire civil doit tenir le fait avoué pour acquis, c'est pour cette raison que l'aveu réalise la concordance des allégations des parties qui, en application du principe dispositif, interdit au juge de fonder sa décision sur un autre moyen de fait. L'irrévocabilité de l'aveu connait deux manifestations, l'une substantielle, par laquelle la preuve est définitivement constituée, l'autre procédurale, qui emporte l'irrecevabilité du moyen de fait contraire à l'aveu. L'indivisibilité de l'aveu peut être analysée comme procédant de la condition suspensive ou résolutoire dont cet acte juridique peul être affecté. / The strength of judicial civil confession is inherited from roman confessio in jure, that was however an admission of claim. Confession being held as an evidence since the medieval law, its nature wears the seal of will whereas its regime is mostly determined by search for the truth. On the one hand, requirement of a free will, both in civil and criminal procedures, grants confession the nature of a legal act intended to prove a fact. Thus genuine confessions can be distinguished from sanctions against litigants who disregard the judge’s imperium, in civil cases as well as in administrative cases. On the other hand, the weight of evidence brought by confession is always determined by the courts in their unfettered discretion. Obligation for civil jurisdictions to state only in consideration of the confessed fact relies on the principle of party disposition. Civil judicial confession 's legal irrevocability is both substantial, as the evidence is permanently constituted, and procedural, preventing the confessor to invoke an opposite allegation of fact. Confession's indivisibility can be analyzed as a result of the suspensive or resolutive condition under which this legal act can be granted.

Cette thèse porte sur la notion de certification locale, un sujet central en décision distribuée, un domaine du calcul distribué. Le mécanisme de la décision distribuée consiste, pour les nœuds d'un réseau, à décider de manière distribuée si le réseau est dans une configuration correcte ou non, selon un certain prédicat. Cette décision est dite locale, car les nœuds du réseau ne peuvent communiquer qu'avec leurs voisins. Après avoir communiqué, chaque nœud prend une décision, exprimant si le réseau est correct ou non localement, c'est-à-dire correct étant donné l'information partielle récoltée jusque-là. Le réseau est déclaré correct globalement s'il est déclaré correct localement par tous les nœuds.Du fait de la contrainte de localité, peu de prédicats peuvent être vérifiés de cette manière. La certification locale est un moyen de contourner cette difficulté, et permet de décider tous les prédicats. C'est un mécanisme qui consiste à étiqueter les nœuds du réseau avec ce que l'on appelle des certificats, qui peuvent être vérifiés localement par un algorithme distribué. Un schéma de certification locale est correct si seuls les réseaux dans une configuration correcte peuvent être certifiés. L'idée de la certification locale est non seulement séduisante d'un point de vue théorique, comme une forme de non-déterminisme distribué, mais c'est surtout un concept très utile pour l'étude des algorithmes tolérants aux pannes, où une étape-clé consiste à vérifier l'état du réseau en se basant sur des informations stockées par les nœuds.Cette thèse porte sur quatre aspects de la certification locale : la sensibilité aux erreurs, l'uniformité, la redondance et l'interactivité. L'étude de ces quatre sujets est motivée par une question essentielle : comment réduire les ressources nécessaires à la certification et/ou permettre une meilleure tolérance aux pannes? Pour aborder cette question, il est nécessaire de comprendre le mécanisme de certification en profondeur. Dans cette optique, dans cette thèse, nous apportons des réponses aux questions suivantes. À quel point les certificats doivent-ils être redondants, pour assurer une certification correcte? Les schémas de certification classiques sont-ils robustes à un changement de la condition de correction? Le fait d'introduire de l'interactivité dans le processus change-t-il la complexité de la certification? / This dissertation is about local certification, a central topic in distributed decision, a subfield of distributed computing. The distributed decision mechanism consists, for the nodes of a network, in deciding in a distributed manner whether the network is in a proper configuration or not, with respect to some fixed predicate. This decision is said to be local because the nodes of the network can communicate only with their neighbours. After communication, every node outputs a decision, stating whether the network is locally correct, that is, correct given the partial information gathered so far by this node. The network is declared to be globally correct, if and only if, it is declared to be locally correct by every node.Most predicates cannot be verified by this type of computation, due to the locality constraint. Local certification is a mechanism that enables to circumvent this difficulty, and to check any property. It consists in providing the nodes of the network with labels, called certificates, that can be verified locally by a distributed algorithm. A local certification scheme is correct if only the networks that satisfy the predicate can be certified. In addition to its theoretical appeal, as a form of distributed non-determinism, the concept of local certification is especially relevant in the study of fault-tolerant distributed algorithms, where a key step consists in checking the status of the network, based on information stored at the nodes.This dissertation deals with four aspects of local certification: error-sensitivity, uniformity, redundancy, and interactivity. The study of these four topics is motivated by the same essential question: How to reduce the resources needed for certification, and/or ensure a better fault-tolerance? In order to tackle this question we have to understand fundamental properties of certification. In particular, in this dissertation we answer questions such as: How redundant the certificates need to be for a proper certification? Are the classic certification protocols robust to a strengthening of the acceptance condition? and, How does introducing interactivity in the process changes the complexity of certification?

Les logiciels critiques nécessitent l’obtention d’une évaluation de conformité aux normesen vigueur avant leur mise en service. Cette évaluation est obtenue après un long travaild’analyse effectué par les évaluateurs de logiciels critiques. Ces derniers peuvent être aidéspar des outils utilisés de manière interactive pour construire des modèles, en faisant appel àdes analyses de flots d’information. Des outils comme SPARK-Ada existent pour des sous-ensembles du langage Ada utilisés pour le développement de logiciels critiques. Cependant,des langages émergents comme ceux de la famille ML ne disposent pas de tels outils adaptés.La construction d’outils similaires pour les langages ML demande une attention particulièresur certaines spécificités comme les fonctions d’ordre supérieur ou le filtrage par motifs. Cetravail présente une analyse de flot d’information pour de tels langages, spécialement conçuepour répondre aux besoins des évaluateurs. Cette analyse statique prend la forme d’uneinterprétation abstraite de la sémantique opérationnelle préalablement enrichie par desinformations de dépendances. Elle est prouvée correcte vis-à-vis d’une définition formellede la notion de dépendance, à l’aide de l’assistant à la preuve Coq. Ce travail constitue unebase théorique solide utilisable pour construire un outil efficace pour l’analyse de toléranceaux pannes. / Critical software needs to obtain an assessment before commissioning in order to ensure compliance tostandards. This assessment is given after a long task of software analysis performed by assessors. Theymay be helped by tools, used interactively, to build models using information-flow analysis. Tools likeSPARK-Ada exist for Ada subsets used for critical software. But some emergent languages such as thoseof the ML family lack such adapted tools. Providing similar tools for ML languages requires specialattention on specific features such as higher-order functions and pattern-matching. This work presentsan information-flow analysis for such a language specifically designed according to the needs of assessors.This analysis is built as an abstract interpretation of the operational semantics enriched with dependencyinformation. It is proved correct according to a formal definition of the notion of dependency using theCoq proof assistant. This work gives a strong theoretical basis for building an efficient tool for faulttolerance analysis.

La Méthode B est une méthode formelle de spécification et de développement de logiciels critiques largement utilisée dans l'industrie ferroviaire. Elle permet le développement de programmes dit corrects par construction, grâce à une procédure de raffinements successifs d'une spécification abstraite jusqu'à une implantation déterministe du programme. La correction des étapes de raffinement est garantie par la vérification de la correction de formules mathématiques appelées obligations de preuve et exprimées dans la théorie des ensembles de la Méthode B. Les projets industriels utilisant la Méthode B génèrent généralement des milliers d'obligation de preuve. La faisabilité et la rapidité du développement dépendent donc fortement d'outils automatiques pour prouver ces formules mathématiques. Un outil logiciel, appelé Atelier B, spécialement développé pour aider au développement de projet avec la Méthode B, aide les utilisateurs a se décharger des obligations de preuve, automatiquement ou interactivement. Améliorer la vérification automatique des obligations de preuve est donc une tache importante. La solution que nous proposons est d'utiliser Zenon, un outils de déduction automatique pour la logique du premier ordre et qui implémente la méthode des tableaux. La particularité de Zenon est de générer des certificats de preuve, des preuves écrites dans un certain format et qui permettent leur vérification automatique par un outil tiers. La théorie des ensembles de la Méthode B est une théorie des ensembles en logique du premier ordre qui fait appel à des schémas d'axiomes polymorphes. Pour améliorer la preuve automatique avec celle-ci, nous avons étendu l'algorithme de recherche de preuve de Zenon au polymorphisme et à la déduction modulo théorie. Ce nouvel outil, qui constitue le cœur de notre contribution, est appelé Zenon Modulo. L'extension de Zenon au polymorphisme nous a permis de traiter, efficacement et sans encodage, les problèmes utilisant en même temps plusieurs types, par exemple les booléens et les entiers, et des axiomes génériques, tels ceux de la théorie des ensembles de B. La déduction modulo théorie est une extension de la logique du premier ordre à la réécriture des termes et des propositions. Cette méthode est parfaitement adaptée à la recherche de preuve dans les théories axiomatiques puisqu'elle permet de transformer des axiomes en règles de réécriture. Par ce moyen, nous passons d'une recherche de preuve dans des axiomes à du calcul, réduisant ainsi l'explosion combinatoire de la recherche de preuve en présence d'axiomes et compressant la taille des preuves en ne gardant que les étapes intéressantes. La certification des preuves de Zenon Modulo, une autre originalité de nos travaux, est faite à l'aide de Dedukti, un vérificateur universel de preuve qui permet de certifier les preuves provenant de nombreux outils différents, et basé sur la déduction modulo théorie. Ce travail fait parti d'un projet plus large appelé BWare, qui réunit des organismes de recherche académique et des industriels autour de la démonstration automatique d'obligations de preuve dans l'Atelier B. Les partenaires industriels ont fournit à BWare un ensemble d'obligation de preuve venant de vrais projets industriels utilisant la Méthode B, nous permettant ainsi de tester notre outil Zenon Modulo.Les résultats expérimentaux obtenus sur cet ensemble de référence sont particulièrement convaincant puisque Zenon Modulo prouve plus d'obligation de preuve que les outils de déduction automatique de référence au premier ordre. De plus, tous les certificats de preuve produits par Zenon Modulo ont été validés par Dedukti, nous permettant ainsi d'être très confiant dans la correction de notre travail. / The B Method is a formal method heavily used in the railway industry to specify and develop safety-critical software. It allows the development of correct-by-construction programs, thanks to a refinement process from an abstract specification to a deterministic implementation of the program. The soundness of the refinement steps depends on the validity of logical formulas called proof obligations, expressed in a specific typed set theory. Typical industrial projects using the B Method generate thousands of proof obligations, thereby relying on automated tools to discharge as many as possible proof obligations. A specific tool, called Atelier B, designed to implement the B Method and provided with a theorem prover, helps users verify the validity of proof obligations, automatically or interactively. Improving the automated verification of proof obligations is a crucial task for the speed and ease of development. The solution developed in our work is to use Zenon, a first-orderlogic automated theorem prover based on the tableaux method. The particular feature of Zenon is to generate proof certificates, i.e. proof objects that can be verified by external tools. The B Method is based on first-order logic and a specific typed set theory. To improve automated theorem proving in this theory, we extend the proof-search algorithm of Zenon to polymorphism and deduction modulo theory, leading to a new tool called Zenon Modulo which is the main contribution of our work. The extension to polymorphism allows us to deal with problems combining several sorts, like booleans and integers, and generic axioms, like B set theory axioms, without relying on encodings. Deduction modulo theory is an extension of first-order logic with rewriting both on terms and propositions. It is well suited for proof search in axiomatic theories, as it turns axioms into rewrite rules. This way, we turn proof search among axioms into computations, avoiding unnecessary combinatorial explosion, and reducing the size of proofs by recording only their meaningful steps. To certify Zenon Modulo proofs, we choose to rely on Dedukti, a proof-checker used as a universal backend to verify proofs coming from different theorem provers,and based on deduction modulo theory. This work is part of a larger project called BWare, which gathers academic entities and industrial companies around automated theorem proving for the B Method. These industrial partners provide to BWare a large benchmark of proof obligations coming from real industrial projects using the B Method and allowing us to test our tool Zenon Modulo. The experimental results obtained on this benchmark are particularly conclusive since Zenon Modulo proves more proof obligations than state-of-the-art first-order provers. In addition, all the proof certificates produced by Zenon Modulo on this benchmark are well checked by Dedukti, increasing our confidence in the soundness of our work.

Le chikungunya, la dengue et la bilharziose urogénitale sont des maladies vectorielles émergentes qui ont récemment trouvé des conditions favorables à leur transmission en France métropolitaine.Santé publique France, l’Agence en charge de la surveillance de l’état de santé de la population française est en première ligne pour détecter et investiguer ces émergences afin d’orienter les mesures de leur prévention et de leur contrôle. Postulant que chaque épidémie constitue une situation d’« expérimentation naturelle », l’objectif de cette thèse était de montrer comment chaque investigation d’épidémie apporte l’opportunité d’acquérir des connaissances scientifiques sur la contribution des cas asymptomatiques à l’introduction, la dissémination et l’endémisation des maladies vectorielles de façon réactive.Notre méta-analyse d’études de séroprévalence per- et post-épidémiques suggère que, contrairement à nos attentes, la lignée de virus chikungunya qui a émergé en 2004 dans l’Océan Indien qui était associée moins d’infections asymptomatiques que les autres. Dans une étude de la séroprévalence de la dengue à Nîmes en 2015, nous avons montré que le potentiel de diffusion de la dengue en France restait actuellement limité. Les données du dépistage des personnes exposées au risque de bilharziose urogénitale en Corse montrant une fréquence élevée d'infections pré-symptomatiques, nous avons évoqué un risque d’endémisation de la maladie qui a justifié son inscription sur la liste des maladies à déclaration obligatoire.Ce travail de thèse démontre qu’une approche pragmatique basée sur une veille sanitaire sensible associée à des investigations épidémiologiques de terrain précoces peut contribuer à aussi bien à la lutte contre les émergences qu’à l’évolution des connaissances. / Conditions recently proved favourable to transmission of emerging vector-borne diseases, chikungunya, dengue and urogenital schistosomiasis in mainland France.Santé publique France, the Agency in charge of public health surveillance in France is at the forefront of detecting and investigating emerging infectious disease in order to guide prevention and control measures. Assuming that each outbreak constitutes a situation of "natural experimentation", the aim of this thesis was to show how outbreak investigations give the opportunity to acquire rapidly scientific knowledge on the contribution of asymptomatic cases to the introduction, dissemination and endemisation of vector-borne diseases.Through a meta-analysis of per and post-epidemic seroprevalence studies,we have shown that the chikungunya virus lineage that emerged in the Indian Ocean in 2004 is associated with a lower frequency of asymptomatic infections. In a dengue serosurvey in Nîmes in 2015, we showed that the diffusion potential of dengue in France is currently limited. Screening data of urogenital bilharziasis in persons exposed in Corsica showed a high frequency of pre-symptomatic infections suggestive of a risk of endemisation of the disease that justified its inclusion on the list of notifiable diseases.This thesis work shows that a pragmatic approach based on sensitive surveillance associated with early field outbreak investigations can significantly contribute to both emerging infections control and the advancement of knowledge.

L'interleukine-6 (IL-6) exerce des propriétés biologiques multiples telles que l'activation des cellules immunocompétentes, l'activation de la réponse inflammatoire et l'hématopoïèse. Produite également par les cellules tumorales, l'IL-6 impacte la prolifération, la différenciation et la survie de ces dernières. L'IL-6 représente donc depuis plusieurs années une cible thérapeutique pertinente. Dans la première partie de ce travail, nous avons exploré une nouvelle piste potentielle pour bloquer l'activité biologique de l'IL-6, en utilisant un antagoniste naturel que notre équipe a identifié dans plusieurs lignées d'adénocarcinomes du rein, à savoir la molécule tronquée tIL-6. Suite à l'évaluation comparée de deux systèmes d'expression (E. coli versus CHO), nous avons retenu les cellules CHO comme source de production de fractions enrichies en tIL-6 par chromatographie de gel d'exclusion. Disposant d'un panel d'adénocarcinomes de rein (ACHN, Caki1, CLB CHA, CLB VER) et d'une lignée érythroleucémique (TF1), l'activité fonctionnelle de tIL-6 in vitro a été étudiée sur (1) la signalisation IL-6 induite, (2) la prolifération cellulaire IL-6 induite, la survie cellulaire et (4) la modulation de l'expression de protéines relevantes de l'apoptose. La molécule tIL-6 bloque la phosphorylation de la tyrosine Tyr705 de STAT3, qui est un des éléments clés de la voie de signalisation de l'IL-6. Nous rapportons également une autre observation nouvelle indiquant que tIL-6 exerce un effet pro-apoptotique sur certaines lignées RCC. Dans la seconde partie de notre étude, l'impact d'un Ac Mo anti IL-6 dans la réversion de la résistance aux cytotoxiques ou à la radiothérapie a été étudié. Nos résultats démontrent que la voie IL-6 ne constituerait pas un mécanisme majeur de résistance / Interleukin-6 (IL-6) plays numerous physiological roles including haematopoiesis, immune response and inflammation, but also plays a role in modulating cell growth, differentiation and survival of tumors cells. The first goal of the present study was to investigate on the potential role of the truncated protein IL-6 (tIL-6) encoded by the spliced IL-6 mRNA discovered in renal carcinoma cells (RCC). The R&D program was designed based on an industrial approach, aiming at reaching the decision stage to enter or not into preclinical development. Firstly two different expression systems were investigated (E. coli versus CHO cell line). The mammalian expression system was selected as the protein source since a recombinant glycosylated tIL-6 with a molecular weight similar to the predicted natural molecule was obtained from enriched fractions following size exclusion chromatography. Secondly by using a cell line panel including renal carcinoma cells (ACHN, Caki-1, CLB CHA, CLB-VER ) and an erythroleucemic cell line (TF1), in vitro tIL-6 functional activity were analyzed on (1) IL-6 induced signaling, (2) IL-6 induced cell proliferation, (3) on cell survival and also (4) on expression of specific set of proteins involved in apoptosis pathways. The truncated IL-6 was found inhibit IL-6 induced STAT3 Tyr705 and to induce apoptosis in some RCC cell lines which could be depending on IL-6 expression. Understanding more precisely the role of natural truncated IL-6 and its impact in cell tumour growth control will be a major issue in the development of innovative approach to antagonize directly or not IL6. The second goal of the present study was to investigate on reversing resistance of cancer cell lines to cytotoxics or ionizing radiations through the use of a monoclonal antibody directed against IL-6. Our data support the fact that IL-6 is not the preponderant actor of cell resistance to cytotoxics and ionizing radiations, which seems to be regulated by a complex network of proteins

L’authenticité est une notion courante, qui est abondamment utilisée dans notre quotidien; qu’il s’agisse de qualifier un geste, une parole ou une personne. L’authenticité se révèle aussi être une notion fondamentale, voire omniprésente, au sein du droit de la preuve civile québécois. Il s’agit en effet d’un élément pivot, qui apparaît autant au moment d’apprécier la recevabilité de la preuve que d’en évaluer la force probante. Le législateur n’a pourtant jamais réellement tenté d’en tracer les contours ni même d’en proposer une définition. Il ne réfère généralement qu’aux effets de l’authenticité, sans toutefois se pencher sur la conceptualisation même de cette notion. Les conséquences en sont pour le moins consternantes : on ne sait pas tout à fait ce qu’est l’authenticité, mais on sait ce que ce n’est pas. C’est donc dans ce contexte que s’inscrit le présent mémoire. Il vise d’abord à déterminer ce en quoi constitue l’authenticité en droit québécois, sur le plan conceptuel. Pour ce faire, un aperçu des traditions juridiques qui ont exercé une influence marquée sur le régime juridique québécois sera réalisé, en insistant particulièrement sur les principes de la tradition civiliste européenne continentale. L’idée de cette approche historique consiste à déterrer les fondements mêmes de l’authenticité en droit québécois, telle que se concevait cette notion avant la révolution technologique. Une fois ses pourtours bien établis, le présent mémoire se penchera ensuite sur les conséquences qu’a entrainées, sur l’authenticité, la réaction législative québécoise concomitante à la révolution technologique. Sans revisiter en profondeur la notion, nous verrons que le législateur a pris une approche de décomposition fonctionnelle, qui permet de mieux en apprécier les fondements. Cette approche nous permettra, par ailleurs, de confirmer que l’authenticité est une notion polymorphe, qui demeure systématiquement associée à la qualité de la preuve, en tout ou en partie. Des effets sur le plan probatoire peuvent découler de cette qualité, mais seulement en certaines circonstances. / Authenticity is a common notion that is used extensively in our daily lives, whether it is to qualify an act, a word, or a person. Authenticity is also a fundamental, even omnipresent, notion in Quebec law of evidence. It is a pivotal element, which appears as much when assessing the admissibility of evidence as when evaluating its probative value. However, the legislator has never really attempted to define it. He generally refers only to the effects of authenticity, without addressing the conceptualization of this notion. The consequences are, to say the least, dismaying: we don't quite know what authenticity is, but we know what it is not. It is therefore in this context that the present thesis takes place. It aims first to determine what constitutes authenticity in Quebec law, from a conceptual standpoint. To do so, an overview of the legal traditions that have had a marked influence on the Quebec legal system will be provided, with particular emphasis on the principles of the continental European civil law tradition. The idea of this historical approach is to unearth the very foundations of authenticity in Quebec law, as this concept existed before the technological revolution. This paper will then examine the consequences of the legislative reaction to the technological revolution on authenticity. Without revisiting the notion in depth, we will see that the legislator has taken a functional decomposition approach to authenticity, which allows us to better appreciate its foundations. Moreover, this approach will allow us to confirm that authenticity is a notion which, although polymorphic, remains systematically associated with the quality of the evidence. Probative effects could emerge from this quality, but only in certain circumstances.