L'objectif de cette thèse est de concevoir des méthodes de décomposition de domaine qui sont robustes même pour les problèmes difficiles auxquels on est confronté lorsqu'on simule des objets industriels ou qui existent dans la nature. Par exemple une difficulté à laquelle est confronté Michelin et que les pneus sont constitués de matériaux avec des lois de comportement très différentes (caoutchouc et acier). Ceci induit un ralentissement de la convergence des méthodes de décomposition de domaine classiques dès que la partition en sous domaines ne tient pas compte des hétérogénéités. Pour trois méthodes de décomposition de domaine (Schwarz Additif, BDD et FETI) nous avons prouvé qu¿en résolvant des problèmes aux valeurs propres généralisés dans chacun des sous domaines on peut identifier automatiquement quels sont les modes responsables de la convergence lente. En d¿autres termes on divise le problème de départ en deux : une partie où on peut montrer que la méthode de décomposition de domaine va converger et une seconde où on ne peut pas. L¿idée finale est d¿appliquer des projections pour résoudre ces deux problèmes indépendemment (c¿est la déflation) : au premier on applique la méthode de décomposition de domaine et sur le second (qu¿on appelle le problème grossier) on utilise un solveur direct qu¿on sait être robuste. Nous garantissons théorétiquement que le solveur à deux niveaux qui résulte de ces choix est robuste. Un autre atout de nos algorithmes est qu¿il peuvent être implémentés en boite noire ce qui veut dire que les matériaux hétérogènes ne sont qu¿un exemple des difficultés qu¿ils peuvent contourner / The objective of this thesis is to design domain decomposition methods which are robust even for hard problems that arise when simulating industrial or real life objects. For instance one particular challenge which the company Michelin is faced with is the fact that tires are made of rubber and steel which are two materials with very different behavior laws. With classical domain decomposition methods, as soon as the partition into subdomains does not accommodate the discontinuities between the different materials convergence deteriorates. For three popular domain decomposition methods (Ad- ditive Schwarz, FETI and BDD) we have proved that by solving a generalized eigenvalue problem in each of the subdomains we can identify automatically which are the modes responsible for slow convergence. In other words we can divide the original problem into two problems : the first one where we can guarantee that the domain decomposition method will converge quickly and the second where we cannot. The final idea is to apply projections to solve these two problems independently (this is also known as deflation) : on the first we apply the domain decomposition method and on the second (we call it the coarse space) we use a direct solver which we know will be robust. We guarantee theoretically that the resulting two level solver is robust. The other main feature of our algorithms is that they can be implemented as black box solvers meaning that heterogeneous materials is only one type of difficulty that they can identify and circumvent.

Le test à base de modèle, en particulier test basé sur des assistants à la preuve, réduit de façon transparente l'écart entre la théorie, le modèle formel, et l’implémentation d'un système informatique. Actuellement, les techniques de tests offrent une possibilité d'interagir directement avec de "vrais" systèmes : via différentes propriétés formelles, les tests peuvent être dérivés et exécutés sur le système sous test. Convenablement, l'ensemble du processus peut être entièrement automatisé. Le but de cette thèse est de créer un environnement de test de séquence à base de modèle pour les programmes séquentiels et concurrents. Tout d'abord une théorie générique sur les monades est présentée, qui est indépendante de tout programme ou système informatique. Il se trouve que notre théorie basée sur les monades est assez expressive pour couvrir tous les comportements et les concepts de tests. En particulier, nous considérons ici : les exécutions séquentielles, les exécutions concurrentes, les exécutions synchronisées, les exécutions avec interruptions. Sur le plan conceptuel, la théorie apporte des notions comme la notion raffinement de test, les cas de tests abstraits, les cas de test concrets, les oracles de test, les scénarios de test, les données de tests, les pilotes de tests, les relations de conformités et les critères de couverture dans un cadre théorique et pratique. Dans ce cadre, des règles de raffinement de comportements et d'exécution symbolique sont élaborées pour le cas générique, puis affinées et utilisées pour des systèmes complexes spécifique. Comme application pour notre théorie, nous allons instancier notre environnement par un modèle séquentiel d'un microprocesseur appelé VAMP développé au cours du projet Verisoft. Pour le cas d'étude sur la concurrence, nous allons utiliser notre environnement pour modéliser et tester l'API IPC d'un système d'exploitation industriel appelé PikeOS.Notre environnement est implémenté en Isabelle / HOL. Ainsi, notre approche bénéficie directement des modèles, des outils et des preuves formelles de ce système. / Formal methods can be understood as the art of applying mathematical reasoningto the modeling, analysis and verification of computer systems. Three mainverification approaches can be distinguished: verification based on deductive proofs,model checking and model-based testing.Model-based testing, in particular in its radical form of theorem proving-based testingcite{brucker.ea:2012},bridges seamlessly the gap between the theory, the formal model, and the implementationof a system. Actually,theorem proving based testing techniques offer a possibility to directly interactwith "real" systems: via differentformal properties, tests can be derived and executed on the system under test.Suitably supported, the entire process can fully automated.The purpose of this thesis is to create a model-based sequence testing environmentfor both sequential and concurrent programs. First a generic testing theory basedon monads is presented, which is independent of any concrete program or computersystem. It turns out that it is still expressive enough to cover all common systembehaviours and testing concepts. In particular, we consider here: sequential executions,concurrent executions, synchronised executions, executions with abort.On the conceptual side, it brings notions like test refinements,abstract test cases, concrete test cases,test oracles, test scenarios, test data, test drivers, conformance relations andcoverage criteria into one theoretical and practical framework.In this framework, both behavioural refinement rules and symbolic executionrules are developed for the generic case and then refined and used for specificcomplex systems. As an application, we will instantiate our framework by an existingsequential model of a microprocessor called VAMP developed during the Verisoft-Project.For the concurrent case, we will use our framework to model and test the IPC API of areal industrial operating system called PikeOS.Our framework is implemented in Isabelle/HOL. Thus, our approach directly benefitsfrom the existing models, tools, and formal proofs in this system.

Cette thèse se positionne dans le domaine de la vérification déductive de programmes, qui consiste à transformer une propriété à vérifier sur un programme en un énoncé logique, pour ensuite démontrer cet énoncé. La vérification effective d'un programme peut poser de nombreuses difficultés pratiques. En fait, les concepts mis en jeu derrière le programme peuvent suffire à faire obstacle à la vérification. En effet, certains programmes peuvent être assez courts et n'utiliser que des constructions simples, et pourtant s'avérer très difficiles à vérifier. Cela nous amène à la question suivante: dans le contexte d'un environnement de vérification déductive de programmes basé sur les démonstrateurs automatiques, quelles méthodes appliquer pour réduire l'effort nécessaire à la fois pour spécifier des comportements attendus complexes, ainsi que pour démontrer qu'un programme respecte ces comportements attendus? Pour mener notre étude, nous nous sommes placés dans le cadre de l'environnement de vérification déductive de programmes Why3. La vérification de programmes en Why3 est basée sur la génération de conditions de vérification, et l'usage de démonstrateurs externes pour les prouver, que ces démonstrateurs soient automatiques ou interactifs. Nous avons développé plusieurs méthodes, certaines générales et d'autres spécifiques à des classes de programmes, pour réduire l'effort manuel. Nos contributions sont les suivantes. Tout d'abord, nous ajoutons des fonctionnalités à Why3 pour assister le processus de vérification, notamment un mécanisme léger de preuve déclarative basé sur la notion d'indicateurs de coupures. Ensuite, nous présentons une méthode de vérification d'absence de débordement arithmétique pour une classe d'utilisation des entiers difficile à traiter par les méthodes standards. Enfin, nous nous intéressons au développement d'une bibliothèque générique pour la spécification et la preuve de programmes générateurs de code. / This thesis is set in the domain of deductive verification of programs, which consists of transforming a property to be verified about a program into a logical statement, and then proving this statement. Effective verification of a program can pose many practical difficulties. In fact, the concepts behind the program may be sufficient to impede verification. Indeed, some programs can be quite short and use only simple constructions, and yet prove very difficult to verify. This leads us to the following question: in the context of a deductive program verification environment based on automatic provers, what methods can be applied to reduce the effort required both to specify complex behaviors, as well as to prove that a program respects these expected behaviors? To carry out our study, we placed ourselves in the context of the deductive verification environment of programs Why3. The verification of programs in Why3 is based on the generation of verification conditions, and the use of external provers to prove them, whether these provers are automatic or interactive. We have developed several methods, some general and others specific to some program classes, to reduce manual effort. Our contributions are as follows. First, we add features to Why3 to assist the verification process, including a lightweight declarative proof mechanism based on the notion of cut indicators. Then we present a method for checking the absence of arithmetic overflow, for use cases which are difficult to process by standard methods. Finally, we are interested in the development of a generic library for the specification and proof of code generating programs.

Le sujet de cette thèse est l’étude de l’encodage des références et de la concurrence dans la Logique Linéaire. Notre motivation est de montrer que la Logique Linéaire est capable d’encoder des effets de bords, et pourrait ainsi servir comme une cible de compilation pour des langages fonctionnels qui soit à la fois viable, formalisée et largement étudiée. La notion clé développée dans cette thèse est celle de zone de routage. C’est une famille de réseaux de preuve qui correspond à un fragment de la logique linéaire différentielle, et permet d’implémenter différentes primitives de communication. Nous les définissons et étudions leur théorie. Nous illustrons ensuite leur expressivité en traduisant un λ-calcul avec concurrence, références et réplication dans un fragment des réseaux différentiels. Pour ce faire, nous introduisons un langage semblable au λ-calcul concurrent d’Amadio, mais avec des substitutions explicites à la fois pour les variables et pour les références. Nous munissons ce langage d’un système de types et d’effets, et prouvons la normalisation forte des termes bien typés avec une technique qui combine la réductibilité et une nouvelle technique interactive. Ce langage nous permet de prouver un théorème de simulation, et un théorème d’adéquation pour la traduction proposée. / The topic of this thesis is the study of the encoding of references andconcurrency in Linear Logic. Our perspective is to demonstrate the capabilityof Linear Logic to encode side-effects to make it a viable, formalized and wellstudied compilation target for functional languages in the future. The keynotion we develop is that of routing areas: a family of proof nets whichcorrespond to a fragment of differential linear logic and which implementscommunication primitives. We develop routing areas as a parametrizable deviceand study their theory. We then illustrate their expressivity by translating aconcurrent λ-calculus featuring concurrency, references and replication to afragment of differential nets. To this purpose, we introduce a language akin toAmadio’s concurrent λ-calculus, but with explicit substitutions for bothvariables and references. We endow this language with a type and effect systemand we prove termination of well-typed terms by a mix of reducibility and anew interactive technique. This intermediate language allows us to prove asimulation and an adequacy theorem for the translation

Les travaux de cette thèse ont pour cadre la vérification formelle, et plus spécifiquement le projet ANR Blanc CLIMT (Categorical and Logical Methods in Model Transformation) dédié aux grammaires de graphes. Ce projet, qui a démarré en février 2012 pour une durée de 48 mois, a donné lieu à la définition du langage Small-tALC, bâti sur la logique de description ALCQI. Ce langage prend la forme d’un DSL (Domain Specific Language) impératif à base de règles, chacune dérivant structurellement un graphe. Le langage s’accompagne d’un composant de preuve basé sur la logique de Hoare chargé d’automatiser le processus de vérification d’une règle. Cependant, force est de constater que tous les praticiens ne sont pas nécessairement familiers avec les méthodes formelles du génie logiciel et que les transformations sont complexes à écrire. En particulier, ne disposant que du seul prouveur, il s’agit pour le développeur Small-tALC d’écrire un triplet de Hoare {P} S {Q} et d’attendre le verdict de sa correction sous la forme d’un graphe contre-exemple en cas d’échec. Ce contre-exemple est parfois difficile à décrypter, et ne permet pas de localiser aisément l’erreur au sein du triplet. De plus, le prouveur ne valide qu’une seule règle à la fois, sans considérer l’ensemble des règles de transformation et leur ordonnancement d’exécution. Ce constat nous a conduits à proposer un environnement d’assistance au développeur Small-tALC. Cette assistance vise à l’aider à rédiger ses triplets et à prouver ses transformations, en lui offrant plus de rétroaction que le prouveur. Pour ce faire, les instructions du langage ont été revisitées selon l’angle ABox et TBox de la logique ALCQI. Ainsi, conformément aux logiques de description, la mise à jour du graphe par la règle s’assimile à la mise à jour ABox des individus (les nœuds) et de leurs relations (les arcs) d’un domaine terminologique TBox (le type des nœuds et les étiquettes des arcs) susceptible d’évoluer. Les contributions de cette thèse concernent : (1) un extracteur de préconditions ABox à partir d’un code de transformation S et de sa postcondition Q pour l’écriture d’une règle {P} S {Q} correcte par construction, (2) un raisonneur TBox capable d’inférer des propriétés sur des ensembles de nœuds transformés par un enchaînement de règles {Pi} Si {Qi}, et (3) d’autres diagnostics ABox et TBox sous la forme de tests afin d’identifier et de localiser des problèmes dans les programmes. L’analyse statique du code de transformation d’une règle, combinée à un calcul d’alias des variables désignant les nœuds du graphe, permet d’extraire un ensemble de préconditions ABox validant la règle. Les inférences TBox pour un enchaînement de règles résultent d’une analyse statique par interprétation abstraite des règles ABox afin de vérifier formellement des états du graphe avant et après les appels des règles. A ces deux outils formels s’ajoutent des analyseurs dynamiques produisant une batterie de tests pour une règle ABox, ou un diagnostic TBox pour une séquence de règles / The overall context of this thesis is formal verification, and more specifically the ANR Blanc CLIMT project (Categorical and Logical Methods in Model Transformation) dedicated to graph grammars. This project, which started in February 2012 for 48 months, gave rise to the development of the Small- tALC language, a graph transformation language based on the ALCQI description logic. This language takes the form of an imperative DSL (Domain Specific Language) based on rules; from each rule structurally derives a graph. It goes with a proof component based on Hoare's logic designed to automate the process of rule verification. However, it must be assumed that not all developers are familiar with formal methods of software engineering, and that graph transformations are complex to write. In particular, using exclusively the prover, the Small- tALC developer must write a Hoare triple {P} S {Q} and wait for the feedback in the form of a counterexample graph in case of failure. This counter-example is sometimes difficult to interpret, and so it does not allow to easily locate the error within the triple. Moreover, the prover validates only one rule at once, without considering all the transformation rules and their execution order. This fact led us to propose an assistance framework for Small- tALC to help developers write their triples and prove their transformations, providing them more feedback than the prover does. To this purpose, the Small- tALC instructions have been reviewed according to the ABox and TBox aspects of the ALCQI logic. Thus, in accordance with description logics, updating the graph by the rule corresponds to the ABox updating of individuals (nodes) and their relationships (edges) of a TBox terminology domain (nodes concepts and edges labels) that is also expected to evolve. The contributions of this thesis concern: (1) an ABox precondition extractor from a transformation code S and its post-condition Q in order to produce a correct by construction rule {P} S {Q}, (2) a TBox reasoner to infer properties on sets of nodes transformed by a rule sequence {Pi} Si {Qi}, and (3) other ABox and TBox diagnostics based on tests to identify and locate errors in programs. The static analysis of the code of a transformation rule, combined with an alias calculus of the variables that can not designate the same nodes of the graph, allows to extract a set of ABox preconditions validating the rule. TBox inferences related to a sequence of rules result from a static analysis by abstract interpretation of the ABox rules. These inferences formally check graph states before and after rule calls. Beside these two formal tools, the framework features dynamic analyzers that produce test cases for an ABox rule, or a TBox diagnosis for a sequence of rules

« Depuis la constatation d'une infraction jusqu'au jugement de son auteur, toute la chaîne pénale est articulée autour de la question cardinale de la preuve ». Placées au coeur du procès pénal, la preuve et son administration sont aujourd'hui confrontées à de nouveaux enjeux. La modernisation de la société et le développement exponentiel des nouveaux moyens de communications et des nouvelles technologies, en tous domaines, bousculent l'administration de la preuve et les règles qui la régissent. Dans un même temps, les droits processuels s'invitent désormais aux côtés des droits fondamentaux, résultat de la place prépondérante prise par la jurisprudence de la Cour européenne des droits de l’homme,mais aussi du droit pénal de l'Union européenne. Aussi, l’administration de la preuve doit profiter de cette période de crise d’identité pour se construire un socle juridique pérenne qui tient compte des nouvelles exigences juridiques, judiciaires et sociétales. Ainsi, l'administration de la preuve doit à la fois conduire à la manifestation de la vérité tout en garantissant les droits et les libertés fondamentales. Ensuite et afin de faire face aux enjeux et aux défis de son temps, l'administration de la preuve doit satisfaire à une double exigence, celle de la qualité et de l'efficacité de la loi. Tel est l'objectif de ces travaux, qui se voulant résolument pragmatiques, ont pour fil rouge la loi n°2011-392 du 14 avril 2011 relative à la garde à vue, et s'appuient sur la pratique judiciaire de la gendarmerie nationale, dont la mission ne se cantonne pas à la seule recherche de la preuve. En effet,cette Institution qui met en pratique quotidiennement les règles relatives à l'administration de la preuve se veut aussi être une force de proposition, notamment lors de la phase de conception de la loi. / Placed at the heart of the penal process, today the evidence and its administration are facing new challenges. The modernisation of society and the exponential development of new means of communication and new technologies in all fields are shaking up the administration of evidence and the rules that govern it. At the same time, procedural rights are now being invoked alongside fundamental rights, as a result of the predominant position taken by the case law of the European Court of Human Rights and also of the European Union's criminal law. Thus, the administration of evidence must take advantage of this period of identity crisis to build a permanent legal basis that takes into account new legal, judicial and societal requirements. Consequently, the administration of evidence must lead both to the manifestation of the truth and to the guarantee of fundamental rights and freedoms. Then, in order to face the challenges and challenges of its time, the administration of evidence must meet two requirements: the quality and effectiveness of the law. This is the purpose of this work, which is resolutely pragmatic and has as its guide in the law no. 2011-392 of 14 April 2011 on custody, are based on the judicial practice of the Gendarmerie Nationale, the mission is not confined to the search for evidence alone. Indeed, on a day-to-day basis, this institution enforces and indulges in the rules of the administration of proof also needing to be a force of proposal, especially during the phase of conception of this law.

L’observation du système nerveux, de son métabolisme et de certaines de ses structures est possible grâce à la neuroimagerie. Une littérature importante issue du « neurodroit » véhicule des imaginaires et des fantasmes relatifs aux possibilités judiciaires qu’offriraient ces technologies. Qu’il s’agisse de détection du mensonge, d’identification cérébrale des individus dangereux ou encore de prédiction de comportements déviants, la neuroimagerie, en l’état actuel des technologies, ne peut pourtant être sérieusement conçue comme pouvant faire l’objet de telles applications. L’utilisation de la neuroimagerie dans le cadre d’expertises est néanmoins une réalité, dans les tribunaux canadiens comme dans la loi française. Cette thèse souligne que les conceptions des technologies dont témoignent les deux systèmes juridiques étudiés s’avèrent lacunaires, ce qui engendre des risques. Elle évoque les conditions du recours à une normativité extra-juridique, la normalisation technique, qui pourrait s’élaborer dans ce contexte controversé, et esquisse les traits d’un dialogue amélioré entre les normativités juridique et technologique. / Neuroimaging allows the observation of the nervous system, of both its metabolism and some of its structures. An important literature in “neurolaw” conveys illusions and fantaisies about the judicial possibilities that imaging technologies would contain. Whether it is about lies detection, cerebral identifications of dangerous individuals through their neurobiology or predictions of criminal behaviors, neuroimaging, in the current state of technologies, can not be seriously conceived as being able to offer such applications. Judicial uses of neuroimaging through expertise are a reality nonetheless, in Canadian courts as in French law. This thesis emphasizes that the conceptions of imaging technologies integrated in the two legal systems studied are incomplete, which creates an important amount of risks. It discusses the conditions for the use of an extra-legal normativity, the international technical standardization, which could be elaborated in this particular and controversial context, and outlines several features of an increased dialogue between legal and technological norms

Dedukti est un cadre logique résultant de la combinaison du typage dépendant et de la réécriture. Il permet d'encoder de nombreux systèmes logiques au moyen de plongements superficiels qui préservent la notion de réduction. Ces traductions de systèmes logiques dans un format commun sont une première étape nécessaire à l'échange de preuves entre ces systèmes. Cet objectif d'interopérabilité des systèmes de preuve est la motivation principale de cette thèse. Pour y parvenir, nous nous inspirons du monde des langages de programmation et plus particulièrement des langages orientés-objet parce qu'ils mettent en œuvre des mécanismes avancés d'encapsulation, de modularité et de définitions par défaut. Pour cette raison, nous commençons par une traduction superficielle d'un calcul orienté-objet en Dedukti. L'aspect le plus intéressant de cette traduction est le traitement du sous-typage. Malheureusement, ce calcul orienté-objet ne semble pas adapté à l'incorporation de traits logiques. Afin de continuer, nous devons restreindre les mécanismes orientés-objet à des mécanismes statiques, plus faciles à combiner avec la logique et apparemment suffisant pour notre objectif d'interopérabilité. Une telle combinaison de mécanismes orientés-objet et de logique est présente dans l'environnement FoCaLiZe donc nous proposons un encodage superficiel de FoCaLiZe dans Dedukti. Les difficultés principales proviennent de l'intégration de Zenon, le prouveur automatique de théorèmes sur lequel FoCaLiZe repose, et de la traduction du langage d'implantation fonctionnel de FoCaLiZe qui présente deux constructions qui n'ont pas de correspondance simple en Dedukti : le filtrage de motif local et la récursivité. Nous démontrons finalement comment notre encodage de FoCaLiZe dans Dedukti peut servir en pratique à l'interopérabilité entre des systèmes de preuve à l'aide de FoCaLiZe, Zenon et Dedukti. Pour éviter de trop renforcer la théorie dans laquelle la preuve finale est obtenue, nous proposons d'utiliser Dedukti en tant que méta-langage pour éliminer des axiomes superflus. / Dedukti is a Logical Framework resulting from the combination ofdependent typing and rewriting. It can be used to encode many logical systems using shallow embeddings preserving their notion of reduction. These translations of logical systems in a common format are a necessary first step for exchanging proofs between systems. This objective of interoperability of proof systems is the main motivation of this thesis.To achieve it, we take inspiration from the world of programming languages and more specifically from object-oriented languages because they feature advanced mechanisms for encapsulation, modularity, and default definitions. For this reason we start by a shallow translation of an object calculus to Dedukti. The most interesting point in this translation is the treatment of subtyping. Unfortunately, it seems very hard to incorporate logic in this object calculus. To proceed, object-oriented mechanisms should be restricted to static ones which seem enough for interoperability. Such a combination of static object-oriented mechanisms and logic is already present in the FoCaLiZe environment so we propose a shallow embedding of FoCaLiZe in Dedukti. The main difficulties arise from the integration of FoCaLiZe automatic theorem prover Zenon and from the translation of FoCaLiZe functional implementation language featuring two constructs which have no simple counterparts in Dedukti: local pattern matching and recursion. We then demonstrate how this embedding of FoCaLiZe to Dedukti can be used in practice for achieving interoperability of proof systems through FoCaLiZe, Zenon, and Dedukti. In order to avoid strengthening to much the theory in which the final proof is expressed, we use Dedukti as a meta-language for eliminating unnecessary axioms.

Si l’étude du formalisme et du consensualisme peut constituer un thème classique du droit français, une confrontation de ces grandes notions du droit privé avec l’électronique est moins commune. Pourtant, la transmission électronique des volontés invite à réfléchir au défi lancé aux principes classiques de formation du contrat. Défi partiellement relevé par le législateur qui, en raison de l’abolition du support papier, a dû harmoniser ces notions. Manifestées par des formes libres ou imposées, les volontés devaient pouvoir circuler en ligne. Sans que le consensualisme ne soit explicitement visé, la rencontre de l’offre avec l’acceptation a été adaptée aux contraintes électroniques. Toutefois, il en résulte une réglementation souffrant d’une terminologie et d’un régime imprécis. Pour l’offre, la profusion du formalisme informatif, sans sanction, et le déni de sa forme écrite sont particulièrement incommodants. Pour l’acceptation, la portée du double-clic ou de l’accusé de réception sont encore incertaines. Concernant le formalisme, la transposition de l’acte sous signature privée et de l’acte authentique a inévitablement contribué à la dénaturation de ces formes. Pour le premier, les traits sont alourdis : comment des mentions manuscrites, supposant un irrémédiable lien physique entre la main de l’auteur et l’écriture, pouvaient-elles se réaliser en ligne sans une consolidation technique ? Pour le second, paradoxalement, son avenir semble conditionné par l’assouplissement du caractère mystique de l’authenticité, pour laisser place à une nouvelle authenticité électronique. D’où la nécessité de perfectionner l’adaptation des notions.Cette dernière fait en réalité surgir un mouvement plus profond. Une fois transposés à l’électronique, le consensualisme et le formalisme paraissent infidèles à leurs conceptions traditionnelles. Aussi, les notions seraient-elles exposées à une véritable transformation. Ce qui ne peut être neutre en droit commun des contrats. Concernant le consensualisme, la hiérarchie créée entre les formes et la discrimination des formes non-électroniques suggèrent un renouvellement de son approche classique. L’élaboration d’un néo-consensualisme est envisagée, faisant apparaître une nouvelle dualité du consensualisme en droit commun. Quant aux formalismes ad validitatem et ad probationem, l’impact de l’électronique se concentre sur leurs rapports mutuels. En ligne, leur dissociation devient impossible. Outre une assimilation textuelle, il y aurait une fusion substantielle des écrits, quel que soit leur rôle juridique. Or, une telle union ravive les couleurs d’un phénomène d’unification connu en droit commun des contrats. Il n’y a, alors, qu’un pas vers l’unité du formalisme.Loin d’une abolition des notions, leur mise à l’épreuve par l’électronique invite finalement à repenser les principes de la formation du contrat. / If the study of formalism and consensualism can constitute a classical theme of French law, a comparison of these great notions of private law with electronics is less common. However, the electronic transmission of wills invites to think about the challenge to the conventional principles of contract formation. A challenge partially raised by the legislator who, because of the abolition of paper support, had to adapt these notions. Wills, expressed by free or imposed forms, had to be able to circulate online. Without consensualism being explicitly targeted, the meeting of supply with acceptance has been adapted to electronic constraints. Nevertheless, the result is a regulation with an unclear terminology and regime. For the offer, the profusion of informative formalism, without sanction, and the denial of its written form are particularly bothersome. For acceptance, the scope of the double-click, or the acknowledgment of receipt, are still uncertain. Concerning formalism, the transposition of the act under private signature and the authentic act inevitably contributed to the denaturation of these forms. For the first, the traits are weighed down: how could handwritten mentions, assuming an irremediable physical link between the author's hand and the writing, be realized online without a technical consolidation? For the second, paradoxically, its future seems conditioned by the relaxation of the mystical character of authenticity, to give way to a new electronic authenticity. Hence the need to perfect the adaptation of notions.It actually causes a deeper movement. Once transposed to electronics, consensualism and formalism seem unfaithful to their traditional conceptions. Also, the notions would be exposed to a real transformation. This can not be neutral in common law contracts. Concerning consensualism, the hierarchy created between forms and the discrimination of non-electronic forms suggest a renewal of its classical approach. The development of a neo-consensualism is envisaged, bringing out a new duality of consensualism in common law. As for the formalisms ad validitatem and ad probationem, the impact of the electronics focuses on their mutual relations. Online, their dissociation becomes impossible. In addition to a textual assimilation, there would be a substantial fusion between the writings, whatever their legal role. However, such a union revives the colors of a unifying phenomenon known in the common law of contracts. There is then only one step towards the unity of formalism.Far from an abolition of notions, their testing by the electronics finally invites to rethink the principles of the formation of the contract.

Cette recherche porte sur les médecins légistes et les expertises qu’ils effectuent sur réquisitions du procureur. Ni collaborateurs occasionnels du juge, ni détenteurs d’un titre de spécialité spécifique, les médecins légistes constituent un corps professionnel à distance à la fois du modèle de l’expertise judiciaire et de celui des spécialités médicales. Ils exercent l’expertise médico-légale à titre principal dans des services hospitaliers dédiés, après avoir suivi un cursus dans une spécialité médicale allant de la médecine générale à l’anatomopathologie, en passant par la médecine du travail et la santé publique.La thèse explore la tension entre expertise judiciaire et spécialité médicale et l’analyse simultanément comme étant inscrite dans le processus de constitution du groupe professionnel des médecins légistes, et comme résidant au cœur d’activités de coproduction des vérités médicale et judiciaire sur les faits. Cette recherche repose sur la mise en place d’un dispositif d’enquête empirique associant des observations ethnographiques, des entretiens et un travail documentaire. Les différents sites étudiés (salles d’autopsies, cabinets médicaux, directions ministérielles, administrations déconcentrées, permanences-parquet, cours d’assises, congrès de médecine légale) sont constitutifs du dispositif médico-légal étudié selon deux plans distincts : le plan des protocoles qui, des ministères aux services, vise à organiser et cadrer les activités médico-légales ; celui des rapports d’expertise établis par les médecins légistes, qu’il s’est agi de suivre depuis les services de médecine légale jusqu’aux tribunaux. La première partie consiste à explorer le plan des protocoles, en étudiant notamment la genèse, l’élaboration et la mise en œuvre d’une réforme de la médecine légale. Elle montre que l’organisation des activités médico-légales a oscillé entre deux définitions de l’expertise médico-légale qui instituent respectivement une figure du médecin expert judiciaire et une figure du légiste spécialiste. La deuxième partie retrace les carrières de ceux qui s’engagent dans l’expertise médico-légale. Elle montre que les postures des médecins vis-à-vis de l’expertise médico-légale dépendent de la façon dont ils ajustent l’exercice de cette activité à leur formation médicale d’origine. Enfin, la troisième partie traite des pratiques des experts et des magistrats du parquet, au sein des organisations où les expertises médico-légales sont produites et utilisées, de l’hôpital au tribunal. Cette ethnographie de l’élaboration des preuves médico-légales révèle les tensions qui apparaissent dans le flux de l’activité du fait des différents cadres que les médecins associent dans leurs explorations des corps violentés.Cette approche mobile du dispositif médico-légal permet de soulever deux enjeux théoriques. D’abord, l’articulation entre le niveau micro des pratiques et le niveau méso des organisations conduit à renouveler l’approche par les segments professionnels. L’étude des processus de segmentation permet ici de déterminer si la médecine légale est une activité pilotée depuis la tutelle judiciaire qui finance et consomme des rapports d’expertise, ou si elle tend à devenir une discipline médicale autonome régulée comme une spécialité depuis l’hôpital. Le deuxième enjeu consiste à étudier les processus de socialisation au dispositif et les pratiques des experts de façon dynamique. En définitive, cette thèse propose d’analyser une pratique tendue entre différents cadres mobilisés en situation, tout en analysant certains déterminants sociaux du jugement médico-légal par l’exploration dynamique de trois échelles distinctes : l’organisation de la médecine légale, la socialisation des médecins légistes et l’activité des professionnels qui produisent et se saisissent des rapports médico-légaux. / This research focuses on medical examiners and the reports they provide upon requisition from Public Prosecutors. Neither occasional collaborators of the judge, nor holders of a specific specialty title, forensic scientists and medical examiners form a professional body that is quite distant from both the judicial expert assessment model and the medical specialty model. They mainly practise the medico-legal expertise in dedicated hospital units, and have undergone a medical university curriculum, with medical specialties ranging from general medicine to anatomopathology, and from occupational medicine to public health.This thesis explores the tension between a judicial expert assessment and a medical specialty, and analyses this tension, simultaneously as being enshrined into the formation process of the occupational group, and as a driving force of the coproduction of medical and judicial truths about facts. The research builds on the implementation of an empirical investigation system, associating ethnographic observations, interviews, and documentation. The different locations that were analysed (autopsy rooms, doctors’ offices, Ministerial directions, decentralised administrations, Public Prosecutors’ committee rooms, congress) constitute a two-level analysis of the medico-legal apparatus: on one hand, the protocol level, where medico-legal activities are organised and supervised, from state-level administrations to local departments; on the other hand, the expert assessment level, where medical examiners were studied from medical examination rooms up to courts of law. The first chapter explores the protocol level, by studying, in particular, the genesis, elaboration and implementation of a forensic medicine reform. It highlights how the organisation of medico-legal activities has been oscillating between two definitions of a medico-legal expertise; these two definitions respectively establish the figure of a judicial expert doctor, and the figure of a forensic specialist. The second chapter focuses on the careers of those who embrace the medico-legal expertise field. It reveals how doctors’ positions on medico-legal expertise are reliant on the way they adjust the practising of this activity to their original medical education. Finally, the third chapter analyses the practices of experts and magistrates from the Public Prosecutor’s department, within the organisations where the medico-legal expert assessments are produced and used, from hospitals to courts of law. This ethnography of how medico-legal evidence is created underlines the tensions that come up within this activity stream, as doctors mix up different frameworks in the way they examine assaulted bodies.This mobile approach of the medico-legal apparatus allows the surfacing of two theoretical concerns. First, the logical hierarchy between the micro level of practises and the meso level of organisations leads to renew the approach for professional segments. Studying segmentation processes is a way of determining if forensic medicine is more driven towards being an activity that is piloted by the judicial administration supervision (which funds and consumes the expert assessments), or towards becoming an autonomous medical discipline with the same regulation mechanisms as a regular hospital specialty. This second concern leads to studying the socialization mechanism as well as the practises of experts in a dynamic way. Ultimately, this thesis proposes to analyse a practise that is stretched between different surroundings in concrete situations, while analysing specific social determining factors of the medico-legal assessment, by dynamically exploring three levels: the organisation of forensic medicine, the socialization of the experts, and the actual activity of the professionals that produce and seize medico-legal assessments.