Cette thèse est consacrée à la complexité basée sur le paradigme des preuves interactives. Les classes ainsi définies ont toutes en commun qu’un ou plusieurs prouveurs, infiniment puissants, tentent de convaincre un vérificateur, de puissance bornée, de l’appartenance d’un mot à un langage. Nous abordons ici le modèle classique, où les participants sont des machines de Turing, et le modèle quantique, où ceux-ci sont des circuits quantiques. La revue de littérature que comprend cette thèse s’adresse à un lecteur déjà familier avec la complexité et l’informatique quantique. Cette thèse présente comme résultat la caractérisation de la classe NP par une classe de preuves interactives quantiques de taille logarithmique. Les différentes classes sont présentées dans un ordre permettant d’aborder aussi facilement que possible les classes interactives. Le premier chapitre est consacré aux classes de base de la complexité ; celles-ci seront utiles pour situer les classes subséquemment présentées. Les chapitres deux et trois présentent respectivement les classes à un et à plusieurs prouveurs. La présentation du résultat ci-haut mentionné est l’objet du chapitre quatre. / This thesis is devoted to complexity theory based on the interactive proof paradigm. All classes defined in this way involve one or many infinitely powerful provers attempting to convince a verifier of limited power that a string belongs to a certain language. We will consider the classical model, in which the various participants are Turing machines, as well as the quantum model, in which they are quantum circuits. The literature review included in this thesis assume that the reader is familiar with the basics of complexity theory and quantum computing. This thesis presents the original result that the class NP can be characterized by a class of quantum interactive proofs of logarithmic size. The various classes are presented in an order that facilitates the treatment of interactive classes. The first chapter is devoted to the basic complexity classes; these will be useful points of comparison for classes presented subsequently. Chapters two and three respectively present classes with one and many provers. The presentation of the result mentioned above is the object of chapter four.

Le but de cette thèse est de spécifier et prouver des programmes avec pointeurs, tels que des programmes C, en utilisant des techniques de raffinement. L'approche proposée permet de faire un compromis entre les techniques complexes qui existent dans la littérature et ce qui est utilisable dans l'industrie, en conciliant légèreté des annotations et restrictions sur les alias. Nous définissons, dans un premier temps, un langage d'étude, qui s'inspire du langage C, et dans lequel le seul type de données mutable possible est le type des structures, auquel on accède uniquement à travers des pointeurs. Afin de structurer nos programmes, nous munissons notre langage d'une notion de module et des concepts issus de la théorie du raffinement tels que les variables abstraites que nous formalisons par des champs modèle, et les invariants de collage. Ceci nous permet d'écrire des programmes structurés en composants. L'introduction des invariants de données dans notre langage soulève des problématiques liées au partage de pointeurs. En effet, en cas d'alias, on risque de ne plus pouvoir garantir la validité de l'invariant de données d'une structure. Nous interdisons, alors l'aliasing (le partage de référence) dans notre langage. Pour contrôler les accès à la mémoire, nous définissons un système de type, basé sur la notion de régions. Cette contribution s'inspire de la théorie du raffinement et a pour but, de rendre les programmes les plus modulaires possible et leurs preuves les plus automatiques possible. Nous définissons, sur ce langage, un mécanisme de génération d'obligations de preuve en proposant un calcul de plus faible précondition incorporant du raffinement. Nous prouvons ensuite, la correction de ce mécanisme de génération d'obligations de preuve par une méthode originale, fondée sur la notion de sémantique bloquante, qui s'apparente à une preuve de type soundness et qui consiste donc, à prouver la préservation puis le progrès de ce calcul. Nous étendons, dans un deuxième temps, notre langage en levant partiellement la restriction liée au partage de références. Nous permettons, notamment, le partage de références lorsqu'aucun invariant de données n'est associé au type structure référencé. De plus, nous introduisons le type des tableaux, ainsi que les variables globales et l'affectation qui ne font pas partie du langage noyau. Pour chacune des extensions citées ci-dessus, nous étendons la définition et la preuve de correction du calcul de plus faible précondition en conséquence. Nous proposons enfin, une implantation de cette approche sous forme d'un greffon de Frama-C (http://frama-c.com/). Nous expérimentons notre implantation sur des exemples de modules implantant des structures de données complexes, en particulier des défis issus du challenge VACID0 (http://vacid. codeplex.com/), à savoir les tableaux creux (Sparse Array) et les tas binaires.

La chirurgie informatisée est une science nouvelle dont le but est de croiser la chirurgie avec les sciences de l’informatique afin d’aboutir à des améliorations significatives dans les deux domaines. Avec l’évolution des nouvelles techniques chirurgicales, une collaboration étroite entre chirurgiens et chercheurs est devenue à la fois inévitable et essentielle à l’optimisation des soins chirurgicaux. L’utilisation de modèles mathématiques est la pierre angulaire de ce nouveau domaine. Cette thèse démontre comment une approche systématique d’un problème clinique nous a amenés à répondre à des questions ouvertes dans le domaine chirurgical en utilisant des modèles mathématiques à grande échelle. De manière générale, notre approche inclut (i) une vision générale du problème, (ii) le ciblage du/des système(s) physiologique(s) à étudier pour y répondre, et (iii) un effort de modélisation mathématique, qui a toujours été poussé par la recherche d’un compromis entre complexité du système étudié et réalité physiologique. Nous avons consacré la première partie de cette thèse à l’optimisation des conditions limites à appliquer à un bio-réacteur utilisé pour démultiplier le tissu pulmonaire provenant d’un donneur. Un modèle géométrique de l’arbre trachéo-bronchique couplé à un modèle de dépôt de soluté nous a permis de déterminer l’ensemble des pressions à appliquer aux pompes servant le bio-réacteur afin d’obtenir une distribution optimale des nutriments à travers les cultures de tissus. Nous avons consacré la seconde partie de cette thèse au problème de resténose des greffes de veines utilisées pour contourner une occlusion artérielle. Nous avons reproduit l’apparition de resténose grâce à plusieurs modèles mathématiques qui permettent d’étudier les preuves cliniques et de tester des hypothèses cliniques avec un niveau croissant de complexité et de précision. Pour finir, nous avons développé un cadre de travail robuste pour tester les effets des thérapies géniques afin de limiter la resténose. Une découverte intéressante a été de constater qu’en contrôlant un groupe de gènes spécifique, la perméabilité à la lumière double après un mois de suivi. Grace aux résultats obtenus, nous avons démontré que la modélisation mathématique peut servir de puissant outil pour l’innovation chirurgicale. / Computational surgery is a new science that aims to intersect surgery and computational sciences in order to bring significant improvements in both fields. With the evolution of new surgical techniques, a close collaboration between surgeons and computational scientists became unavoidable and also essential to optimize surgical care. A large usage of mathematical models is the cornerstone in this new field. The present thesis shows how a systematic approach to a clinical problem brought us to answer open questions in the field of surgery by using mathematical models on a large scale. In general, our approach includes (i) an overview of the problem, (ii) the individuation of which physiological system/s is/are to be studied to address the question, and (iii) a mathematical modeling effort, which has been always driven by the pursue of a compromise between system complexity and closeness to the physiological reality. In the first part, we focused on the optimization of the boundary conditions to be applied to a bioreactor used to re-populate lung tissue from donor. A geometrical model of tracheobronchial tree combined with a solute deposition model allowed us to retrieve the set of pressures to be applied to the pumps serving the bioreactor in order to reach an optimal distribution of nourishment across the lung scaffold. In the second part, we focused on the issue of post-surgical restenosis of vein grafts used to bypass arterial occlusions. We replicated the event of restenosis with several mathematical models that allow us to study the clinical evidences and to test hypothesis with an escalating level of complexity and accuracy. Finally, we developed a solid framework to test the effect of gene therapies aimed to limit the restenosis. Interestingly, we found that by controlling a specific group of genes, the lumen patency is double after a month of follow-up. With the results achieved, we proved how mathematical modeling can be used as a powerful tool for surgical innovation.

L’émergence de la logique de performance marque un changement majeur dans les stratégies publiques ou privées de management des ressources humaines. La relation médicale est exemplaire de cette évolution. Alors qu’historiquement les négociations entre l’Etat et les médecins portaient exclusivement sur des problématiques de prix, depuis le début des années 1990, la régulation publique se fait par les pratiques. L’objectif du contrôle est alors de promouvoir la qualité des soins – notamment sur les enjeux de santé publique – et la réduction des dépenses – en évitant le développement des maladies chroniques et en favorisant la prescription de médicaments génériques. L’introduction d’un dispositif de paiement à la performance médicale, en 2011, est l’étape ultime de ce tournant métrologique de la profession qui conduit à multiplier les dispositifs d’évaluation chiffrée de la pratique médicale et à mettre en indicateurs le travail du médecin. Dans une perspective institutionnaliste, notre thèse propose d’interroger la pertinence de cette réforme visant à instituer la performance.Nous montrons que cette institution de la performance n’est ni efficace ni efficiente. En conduisant à de nombreux effets pervers, elle se fait au détriment des intérêts des patients et des médecins de première ligne. L’injonction à la performance ne conduit pas à améliorer la qualité des soins et à renforcer la maîtrise des dépenses de santé, contrairement aux objectifs annoncés. Par contre, dans l’esprit du néolibéralisme contemporain, la santé est assimilée à un bien comme un autre autour duquel il est possible de mettre en concurrence les producteurs et les consommateurs. / The emergence of the logic of performance illustrates a major change in public or private human resources management strategies. The health care relation is exemplary of these evolutions. Historically, negotiations between the State and physicians exclusively focused on prices. However, since the beginning of the 90’s, public regulation is carried out through professional norms. The goal is to improve the quality of care and to control public spending (avoiding chronic diseases and encouraging the use of generic drugs). The introduction of pay-for-performance in France in 2011 is the ultimate stage in this metrological turning point defined by a numerically-based assessment of medical work. In an institutionalist viewpoint, our thesis seeks to question the relevance of this reform which aims at instituting performance.We show that this project is neither effective nor efficient. Leading to numerous perverse effects, it is implemented regardless of the patients’ interests and of the general practitioners. Contrary to what was proclaimed, this injunction for performance did not achieve the improvement of quality in medical care and the control of health expenditures. Yet, in the contemporary neoliberalism spirit, health is associated with a good as any other, surrounding which it is possible to generate competition among producers and consumers.

Dans cette thèse, nous étudions les constructions cryptographiques prouvées pour la protection de la vie privée. Pour cela nous nous sommes intéressés aux preuves et arguments à divulgation nulles de connaissance et leurs applications. Un exemple de ces constructions est la signature de groupe. Ce protocole a pour but de permettre à un utilisateur de s'authentifier comme appartenant à un groupe, sans révéler son identité. Afin que les utilisateurs restent responsable de leurs agissements, une autorité indépendante est capable de lever l'anonymat d'un utilisateur en cas de litige. Une telle construction peut ainsi être utilisée, par exemple, dans les systèmes de transport en commun. Un utilisateur qui rentre dans un bus prouve ainsi son appartenance aux utilisateurs possédant un abonnement valide, sans révéler qui il est, et évitant ainsi que la société de transport ne le trace. En revanche, en cas d'incident sur le réseau, la société peut faire appel à la police pour lever l'anonymat des usagers présents au moment de l'incident. Nous avons proposé deux constructions de ces signatures de groupe, prouvées sûres sous des hypothèses simples dans le monde des couplages et des réseaux euclidiens. Dans la continuité de ces travaux, nous avons aussi proposé la première construction de chiffrement de groupe (l'équivalent de la signature de groupe pour le chiffrement) à base de réseaux euclidiens. Finalement, ces travaux nous ont amené à la construction d'un schéma de transfert inconscient adaptatif avec contrôle d'accès à base de réseaux euclidiens. Ces constructions à base de réseaux ont été rendues possibles par des améliorations successives de l'expressivité du protocole de Stern, qui reposait initialement sur la difficulté du problème du décodage de syndrome. / In this thesis, we study provably secure privacy-preserving cryptographic constructions.We focus on zero-knowledge proofs and their applications.Group signatures are an example of such constructions.This primitive allows users to sign messages on behalf of a group (which they formerly joined), while remaining anonymous inside this group.Additionally, users remain accountable for their actions as another independent authority, a judge, is empowered with a secret information to lift the anonymity of any given signature.This construction has applications in anonymous access control, such as public transportations.Whenever someone enters a public transportation, he signs a timestamp. Doing this proves that he belongs to the group of people with a valid subscription.In case of problem, the transportation company hands the record of suspicious signatures to the police, which is able to un-anonymize them.We propose two constructions of group signatures for dynamically growing groups. The first is based on pairing-related assumptions and is fairly practical. The second construction is proven secure under lattice assumptions for the sake of not putting all eggs in the same basket.Following the same spirit, we also propose two constructions for privacy-preserving cryptography.The first one is a group encryption scheme, which is the encryption analogue of group signatures. Here, the goal is to hide the recipient of a ciphertext who belongs to a group, while proving some properties on the message, like the absence of malwares. The second is an adaptive oblivious transfer protocol, which allows a user to anonymously query an encrypted database, while keeping the unrequested messages hidden.These constructions were made possible through a series of work improving the expressiveness of Stern's protocol, which was originally based on the syndrome decoding problem.

Le langage mathématique courant et les langages mathématiques formelssont très éloignés. Par <<langage mathématique courant>> nousentendons la prose que le mathématicien utilise tous les jours dansses articles et ses livres. C'est une langue naturelle avec desexpressions symboliques et des notations spécifiques. Cette langue està la fois flexible et structurée mais reste sémantiquementintelligible par tous les mathématiciens.Cependant, il est très difficile de formaliser automatiquement cettelangue. Les raisons principales sont: la complexité et l'ambiguïté deslangues naturelles en général, le mélange inhabituel entre languenaturelle et notations symboliques tout aussi ambiguë et les sautsdans le raisonnement qui sont pour l'instant bien au-delà descapacités des prouveurs de théorèmes automatiques ou interactifs.Pour contourner ce problème, les assistants de preuves actuelsutilisent des langages formels précis dans un système logique biendéterminé, imposant ainsi de fortes restrictions par rapport auxlangues naturelles. En général ces langages ressemblent à des langagesde programmation avec un nombre limité de constructions possibles etune absence d'ambiguïté.Ainsi, le monde des mathématiques est séparé en deux, la vastemajorité qui utilise la langue naturelle et un petit nombre utilisantaussi des méthodes formelles. Cette seconde communauté est elle-mêmesubdivisée en autant de groupes qu'il y a d'assistants de preuves. Onperd alors l'intelligibilité des preuves pour tous les mathématiciens.Pour résoudre ce problème, on peut se demander:est-il possible d'écrire un programme qui comprend la langue naturellemathématique et qui la traduit vers un langage formel afin depermettre sa validation?Ce problème se subdivise naturellement en deux sous-problèmes tous lesdeux très difficiles:1. l'analyse grammaticale des textes mathématiques et leur traductiondans un langage formel,2. la validation des preuves écrites dans ce langage formel.Le but du projet MathNat (Mathematics in controlled Natural languages)est de faire un premier pas pour répondre à cette question trèsdifficile, en se concentrant essentiellement sur la première question.Pour cela, nous développons CLM (Controlled Language for Mathematics)qui est un sous-ensemble de l'anglais avec une grammaire et un lexiquerestreint, mais qui inclut tout de même quelques ingrédientsimportants des langues naturelles comme les pronoms anaphoriques, lesréférences, la possibilité d'écrire la même chose de plusieursmanières, des adjectifs distributifs ou non, ...Le second composant de MathNath est MathAbs (Mathematical Abstractlanguage). C'est un langage formel, indépendant du choix d'un systèmelogique permettant de représenter la sémantique des textes enpréservant leur structure et le fil du raisonnement. MathAbs est conçucomme un langage intermédiaire entre CLM et un système logique formelpermettant la vérification des preuves.Nous proposons un système qui permet de traduire CLM vers MathAbsdonnant ainsi une sémantique précise à CLM. Nous considèrons que cetravail est déjà un progrès notable, même si pour l'instant on estloin de pouvoir vérifier formellement toutes les preuves en MathAbsainsi générées.Pour le second problème, nous avons réalisé une petite expérience entraduisant MathAbs vers une liste de formules en logique du premierordre dont la validité garantit la correction de la preuve. Nous avonsensuite essayé de vérifier ces formules avec des prouveurs dethéorèmes automatiques validant ainsi quelques exemples. / There is a wide gap between the language of mathematics and itsformalized versions. The term "language of mathematics" or"mathematical language" refers to prose that the mathematician uses inauthoring textbooks and publications. It mainly consists of naturallanguage, symbolic expressions and notations. It is flexible,structured and semantically well-understood by mathematicians.However, it is very difficult to formalize it automatically. Some ofthe main reasons are: complex and rich linguistic features of naturallanguage and its inherent ambiguity; intermixing of natural languagewith symbolic mathematics causing problems which are unique of itskind, and therefore, posing more ambiguity; and the possibility ofcontaining reasoning gaps, which are hard to fill using the currentstate of art theorem provers (both automated and interactive).One way to work around this problem is to abandon the use of thelanguage of mathematics. Therefore in current state of art of theoremproving, mathematics is formalized manually in very precise, specificand well-defined logical systems. The languages supported by thesesystems impose strong restrictions. For instance, these languages havenon-ambiguous syntax with a limited number of possible syntacticconstructions.This enterprise divides the world of mathematics in two groups. Thefirst group consists of a vast majority of mathematicians whose relyon the language of mathematics only. In contrast, the second groupconsists of a minority of mathematicians. They use formal systems suchas theorem provers (interactive ones mostly) in addition to thelanguage of mathematics.To bridge the gap between the language of mathematics and itsformalized versions, we may ask the following gigantic question:Can we build a program that understands the language of mathematicsused by mathematicians and can we mechanically verify its correctness?This problem can naturally be divided in two sub-problems, both very hard:1. Parsing mathematical texts (mainly proofs) and translating thoseparse trees to a formal language after resolving linguistic issues.2. Verification of this formal version of mathematics.The project MathNat (Mathematics in controlled Natural language) aimsat being the first step towards solving this problem, focusing mainlyon the first question.First, we develop a Controlled Language for Mathematics (CLM) which isa precisely defined subset of English with restricted grammar anddictionary. To make CLM natural and expressive, we support some richlinguistic features such as anaphoric pronouns and references,rephrasing of a sentence in multiple ways and the proper handling ofdistributive and collective readings.Second, we automatically translate CLM to a system independent formaldescription language (MathAbs), with a hope to make MathNat accessibleto any proof checking system. Currently, we translate MathAbs intoequivalent first order formulas for verification.

Dans cette thèse, nous visons à formaliser les effets calculatoires. En effet, les langages de programmation les plus utilisés impliquent différentes sortes d'effets de bord: changement d'état, exceptions, entrées / sorties, non-déterminisme, etc. Ils peuvent apporter facilité et flexibilité dans le processus de codage. Cependant, le problème est de prendre en compte les effets lorsque l'on veut prouver des propriétés de programmes. La principale difficulté dans ce genre de preuve de programmes est le décalage entre la syntaxe des opérations avec effets de bord et leur interprétation. Typiquement, un fragment de programme avec des arguments de type X qui retourne une valeur de type Y n'est pas interprété comme une fonction de X vers Y , à cause des effets.L'approche algébrique la plus connue pour ce problème permet une interprétation des programmes, y compris ceux comportant des effets, en utilisant des monades : l'interprétation est une fonction de X vers T (Y ) où T est une monade. Cette approche a été étendue aux théories de Lawvere et aux "gestionnaires algébriques" (algebraic handlers). Une autre approche, appelée logique décorée, fournit une sémantique équationnelle pour ces programmes. Nous spécialisons l'approche de la logique décorée pour les effets liés à l'état de la mémoire et à la gestion des exceptions en définissant la logique décorée pour les états (L_st) et la logique décorée pour les exceptions (L_exc), respectivement. Elles nous permettent de prouver des propriétés de programmes impliquant de tels effets. Ensuite, nous formalisons ces logiques en Coq et certifions les preuves associées. Ces logiques sont construites de manière à être correctes. En outre, nous introduisons une notion de complétude syntaxique relative d'une théorie dans une logique donnée par rapport à une sous-logique. Nous montrons que la théorie décorée pour les états globaux ainsi que deux théories décorées pour les exceptions sont relativement complets relativement à leur sous-logique pure. Non seulement nous pouvons utiliser le système développé pour prouver des programmes comportant des effets, mais également nous utilisons cette formalisation pour certifier les résultats de complétude obtenus. / In this thesis, we aim to formalize the effects of a computation. Indeed, most used programming languages involve different sorts of effects: state change, exceptions, input/output, non-determinism, etc. They may bring ease and flexibility to the coding process. However, the problem is to take into account the effects when proving the properties of programs. The major difficulty in such kind of reasoning is the mismatch between the syntax of operations with effects and their interpretation. Typically, a piece of program with arguments in X that returns a value in Y is not interpreted as a function from X to Y , due to the effects. The best-known algebraic approach to the problem interprets programs including effects with the use of monads: the interpretation is a function from X to T(Y) where T is a monad. This approach has been extendedto Lawvere theories and algebraic handlers. Another approach called, the decorated logic, provides a sort of equational semantics for reasoning about programs with effects. We specialize the approach of decorated logic to the state and the exceptions effects by defining the decorated logic for states (L_st) and the decorated logic for exceptions (L_exc), respectively. This enables us to prove properties of programs involving such effects. Then, we formalize these logics in Coq and certify the related proofs. These logics are built so as to be sound. In addition, we introduce a relative notion of syntactic completeness of a theory in a given logic with respect to a sublogic. We prove that the decorated theory for the global states as well as two decorated theories for exceptions are syntactically complete relatively to their pure sublogics. These proofs are certified in Coq as applications of ourgeneric frameworks.

En se fondant sur les travaux de Trimble et al., puis Hughes, on donne une notion de théorie symétrique monoïdale close (smc) et une construction explicite de la catégorie smc engendrée, formant ainsi une adjonction entre théories et catégories. On étudie les exemples du lambda-calcul pur linéaire, du lambda-calcul pur standard, puis des bigraphes de Milner. À chaque fois on donne une théorie smc et on compare la catégorie smc engendrée avec la présentation standard. Entre autres, dans les trois cas, on montre une équivalence entre les deux sur les termes clos. / From the work of Trimble et al. and Hughes, we define a notion of symmetric monoidal closed (smc) theory and give an explicit construction of the smc category generated by it. This construction yields a monadic adjunction between smc theories and smc categories. We study in our algebraic framework different models of programming languages: the linear λ-calculus, the pure λ-calculus and Milner's bigraphs. For each model, we give a smc theory and compare the generated smc category with the standard presentation. We show that, in each case, there is an equivalence on closed terms.

En 1908, les juges de la Cour Suprême des États-Unis citent pour la première fois des études en médecine, en sociologie et en psychologie afin de valider la constitutionnalité d’une loi. Depuis, le recours aux preuves scientifiques s’est largement développé et il a pris une place dans le travail du juge aux États-Unis et au Canada. La preuve scientifique se présente comme un outil d’information essentiel pour le juge dans le contentieux constitutionnel des droits et libertés. Elle permet ainsi de décrire les réalités sociales et les aspects techniques qui intéressent directement la résolution des questions constitutionnelles. Au delà de son rôle d'information, son recours s’inscrit dans une logique de concrétisation de l’analyse constitutionnelle. Plus précisément, les critères du contrôle de constitutionnalité impliquent des questions de faits que la preuve scientifique pourra démontrer. En prenant ainsi un tout autre rôle, le recours aux preuves scientifiques questionne sur la nature du contrôle de constitutionnalité et sur les méthodes du juge. Malgré l’intérêt des juges américain et canadien pour ce mode de preuve, leur statut et leur régime juridique dans le contentieux constitutionnel demeurent indéterminés. Ces incertitudes touchent tant des questions de procédure que des questions de fond sur leur rôle dans l’analyse constitutionnelle et dans le raisonnement du juge. Dès lors, la recherche d'un cadre méthodologique a semblé nécessaire. Ce modèle permet de revaloriser l’apport des preuves scientifiques dans le contentieux constitutionnel et il contribue à la protection des droits et libertés. Il présente, alors, un intérêt pour l'ensemble juges constitutionnels / In 1908, the U.S. Supreme Court Justices made several citations of medical, sociology andpsychology studies for the first time. Since then, the use of scientific evidence has expanded and it became an important part of the work of the Supreme Court of the U.S. as well as the Supreme Court of Canada. Scientific evidence is an essential tool to inform judges in constitutional rights cases. It gives information on social realities and technical questions which are directly relevant to resolve questions of law. However, the use of scientific evidence is more than a medium of information. Indeed, it implies an interest for facts that go beyond the parties. Constitutional doctrine itself implies empirical questions that could find answers in scientific evidence. By determining those facts, scientific evidence becomes a part of the constitutional doctrineitself. Consequently, the use of scientific evidence interrogates on the nature of judicial review and on the judge’s methods. Thought judges in the U.S. and in Canada frequently cite scientific evidence, their use is mostly unregulated and indeterminate. The uncertainties surrounding the use of scientific evidence concern procedural questions as well as questions regarding their role in decisionmaking. Those questions must be answered. Once resolved, we research a methodological framework in which scientific evidence could be used consistently by American and Canadian judges. This approach is essential to reassert the value of scientific evidence in constitutionalrights cases and to improve constitutional rights protection. Finally, this framework might be relevant for judges beyond the United States and Canada

Les méthodes formelles ont atteint un degré de maturité conduisant à la conception de systèmes de preuves généralistes, permettant à la fois de vérifier la correction de systèmes logiciels complexes ou de formaliser des mathématiques avancées. Mais souvent, l'accent est mis davantage sur la facilité du raisonnement sur les programmes plutôt que sur leur exécution efficace. L'antagonisme entre ces deux aspects est particulièrement sensible pour les algorithmes de calcul formel, dont la correction repose habituellement sur des concepts mathématiques élaborés, mais dont l'efficacité pratique est une préoccupation importante. Cette thèse développe des approches à l'étude formelle et l'exécution efficace de programmes en théorie des types, et plus précisément dans l'assistant à la preuve \coq{}. Dans un premier temps, nous présentons un environnement d'exécution permettant de compiler en code natif de tels programmes tout en conservant la généralité et l'expressivité du formalisme. Puis, nous nous intéressons aux représentations de données et plus particulièrement au lien formellement vérifié et automatisé entre représentations adaptées aux preuves ou au calcul. Ensuite, nous mettons à profit ces techniques pour l'étude d'algorithmes en algèbre linéaire, comme le produit matriciel de Strassen, le procédé d'élimination de Gauss ou la mise en forme canonique de matrices, dont notamment la forme de Smith pour les matrices sur un anneau euclidien. Enfin, nous ouvrons le champ des applications à la formalisation et au calcul certifié des groupes d'homologie de complexes simpliciaux issus d'images numériques. / Formal methods have reached a degree of maturity leading to the design of general-purpose proof systems, enabling both to verify the correctness of complex software systems and to formalize advanced mathematics. However, the ease of reasoning on programs is often emphasized more than their efficient execution. The antagonism between these two aspects is particularly significant for computer algebra algorithms, whose correctness usually relies on elaborate mathematical concepts, but whose practical efficiency is an important matter of concern. This thesis develops approaches to the formal study and the efficient execution of programs in type theory, and more precisely in the proof assistant \coq{}. In a first part, we introduce a runtime environment enabling the native code compilation of such programs while retaining the generality and expressiveness of the formalism. Then, we focus on data representations and in particular on the formally verified and automatized link between proof-oriented and computation-oriented representations. Then, we take advantage of these techniques to study linear algebra algorithms, like Strassen's matrix product, Gaussian elimination or matrix canonical forms, including the Smith normal form for matrices over a Euclidean ring. Finally, we open the field of applications to the formalization and certified computation of homology groups of simplicial complexes arising from digital images.