Thèse de doctorat : Informatique : Nancy 1 : 2009. / Titre provenant de l'écran-titre.

Dans cette thèse nous présentons la formalisation de trois résultats principaux que sont la forme normale de Jordan d’une matrice, le théorème de Bolzano-Weierstraß et le théorème de Perron-Frobenius. Pour la formalisation de la forme normale de Jordan nous introduisons différents concepts d’algèbre linéaire tel que les matrices diagonales par blocs, les matrices compagnes, les facteurs invariants, ... Ensuite nous définissons et développons une théorie sur les espaces topologiques et métriques pour la formalisation du théorème de Bolzano-Weierstraß. La formalisation du théorème de Perron-Frobenius n’est pas terminée. La preuve de ce théorème utilise des résultats d’algèbre linéaire, mais aussi de topologie. Nous montrerons comment les précédents résultats seront réutilisés. / In this thesis we present the formalization of three principal results that are the Jordan normal form of a matrix, the Bolzano-Weierstraß theorem, and the Perron-Frobenius theorem. To formalize the Jordan normal form, we introduce many concepts of linear algebra like block diagonal matrices, companion matrices, invariant factors, ... The formalization of Bolzano-Weierstraß theorem needs to develop some theory about topological space and metric space. The Perron-Frobenius theorem is not completly formalized. The proof of this theorem uses both algebraic and topological results. We will show how we reuse the previous results.

Bien que non répertorié dans le code civil au titres des modes de preuve admissibles, le constat d'huissier de justice n'en demeure pas moins un outil de référence dans l'établissement de la preuve des faits juridiques. La souplesse de son régime, à laquelle participe notamment la liberté dévolue au constatant dans la relation matérielle, en fait un procédé probatoire malléalble, adapté aux situations les plus diverses. Instrument de prévention des litiges, voire de règlement anticipé de ces derniers, le constat peut aussi permettre au plaideur de satisfaire à la charge processuelle qui lui incombe de rapporter la preuve des faits au soutien de ses prétentions. A cet égard, il constitue assurément un moyen de réalisation du droit à la preuve, entendu comme celui d'imposer au juge une offre ou une demande de preuve présentant un intérêt probatoire légitime et récemment consacré par la jurisprudence sur le fondement de l'article 6 de la Convention européenne des droits de l'homme. L'absence de carcan juridique enfermant la réalisation de la mesure de constat pourrait cependant faire douter de la qualité de celle-ci. L'allégation mérite d'être éprouvée au regard de la qualité particulière de son auteur. Indifférent à la règlementation sporadique de la mesure, l'huissier de justice en garantit une réalisation licite, respectueuse des principes directeurs du procès et des droits subjectifs des tiers. Le renforcement en matière civile de la valeur probante des constatations établies par cet officier ministériel est à ce titre une confirmation officielle de leur qualité indiscutable. / Although not listed in the civil code in conformance with the approved modes of evidences, the statement of ofacts drawn up by a judicial officer is still a reference tool in the establishment of the proof of legal facts. The flexibility of its regime, in which participates in particular the freedom devolved in the material relation, makes it a probationary process moldable, adapted to the most diverse situations. Instrument of prevention of the disputes, or of their advance settlement, the statement of facts can also allow the litigant to satisfy the procedural burden which falls to him to prove the facts to the support of its claims. In this respect, it serves undoubtedly as a means of realization of the right to evidence, settled as the right to impose to the judge an offer or a request of evidence that hold a legitimate probative interest and recently confirmed by case-law on the basis of the Article 6 of the European Convention on Human Rights. The absence of legal straightjacke locking the establishment of the statement of facts could however raise doubts about its quality. This allegation deserves to be felt with regard to the particular quality of the judicial officer. Indifferent to the sporadic regulations of the measure, he guarantees its lawful realization according to the general principles of the trial and the subjective rights third parties. The strengthening in civil maters of the probative value of the findings made by the judicial officer is as such an official confirmation of their indisputable quality.

Notre travail aborde une question technique et difficile de droit pénal international: le traitement de la preuve par ouï-dire en droit international. La question semble peut être, avoir été déjà traitée en droit interne et en droit international. Cependant, en tenant compte des différentes affaires examinées devant le TPIY et TPIR, il n'en demeure pas moins que les preuves par ouï-dire demeurent encore un sujet controversé et préoccupant. En effet, la preuve par ouï-dire devant les tribunaux ad hoc soulève des questions pertinentes concernant d'une part, le principe du procès équitable, les règles du procès pénal, le processus de la recherche de la vérité et constitue d'autre part une source d'incompréhension, générant des conflits subtils entre les juges, avocats et auteurs issus de systèmes juridiques différents. Une analyse critique de la jurisprudence internationale et ses solutions quant à son approche à l'égard du ouï-dire démontre que les juges appliquent essentiellement le droit issu des deux grands systèmes occidentaux: la common law et le droit romano-germanique. Cela nous amène à poser le problème de la compatibilité de la justice internationale qui est calquée sur la tradition du procès accusatoire et celle du procès inquisitoire, et le défis d'un modèle international hégémonique (universel) avec la question de la diversité des traditions juridiques. Ainsi, se pose la question à savoir: est-ce qu'une justice pénale internationale de nature occidentale est légitime, voire compréhensible pour les justiciables appartenant à d'autres cultures? D'où est tiré le titre de notre travail: "L'élaboration des règles de preuve et de procédure au niveau des tribunaux pénaux internationaux dans un contexte de diversité des systèmes juridiques nationaux: le cas du ouï-dire". L'exemple de la preuve par ouï-dire a été fait dans le but de montrer que le droit de la preuve est loin de se rapprocher même au niveau des droits occidentaux, malgré toutes les tendances à l'harmonisation. Nous sommes d'avis qu'une procédure pénale internationale efficace devra prendre en compte les différentes manifestations du droit en repérant les divergences et les convergences entre les divers systèmes de droit en vue d'une réelle harmonisation du droit de la preuve au niveau universel. Nous avons examiné une question importante et toujours d'actualité, le développement vers une hybridation des systèmes civilistes et de common law en droit pénal international. Cet examen nous a permis de faire un aperçu des questions et des problèmes. Quelques remarques concernant le degré de cette mixité, ses implications. Nous avons conclu une discussion sur la diversité culturelle. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Ouï-dire, Procès pénal, Admissibilité, Modèle accusatoire, Modèle inquisitoire, Common law, Droit romano-germanique, Procès équitable, Divergences, Preuve, Procédure, Droit pénal international, Système juridique, Diversité culturelle, Fiabilité, Pertinence, Légitimité, Procédure pénale internationale, Mixité, Hybridation, Harmonisation.

Texte remanié de: Thèse de doctorat--Histoire du droit--Paris 2. / Bibliogr. p. 21-68. Index.

Dans cette thèse nous présentons la formalisation de trois résultats principaux que sont la forme normale de Jordan d'une matrice, le théorème de Bolzano-Weierstraß et le théorème de Perron-Frobenius. Pour la formalisation de la forme normale de Jordan nous introduisons différents concepts d'algèbre linéaire tel que les matrices diagonales par blocs, les matrices compagnes, les facteurs invariants, ... Ensuite nous définissons et développons une théorie sur les espaces topologiques et métriques pour la formalisation du théorème de Bolzano-Weierstraß. La formalisation du théorème de Perron-Frobenius n'est pas terminée. La preuve de ce théorème utilise des résultats d'algèbre linéaire, mais aussi de topologie. Nous montrerons comment les précédents résultats seront réutilisés.

Même si elle n’est pas une preuve per se, il est admis de longue date que la présomption peut, provisoirement, faire office de preuve lorsqu’une preuve directe d’un fait est indisponible ou difficile à produire. En l’absence d’un droit de la preuve codifié de l’Union européenne, il n’est pas aisé d’affirmer que les critères de classification des présomptions en droit interne (l’admissibilité de la preuve et l’auteur de la présomption) sont transposables au droit de l’Union. Cela ne signifie pas que la présomption est irrévocablement bannie du vocabulaire juridique de celle-ci ; l’examen de la jurisprudence de la Cour de justice et du droit en vigueur permet d’identifier un certain nombre de circonstances dans lesquelles le législateur et le juge sont amenés à former des présomptions. La pratique en droit de l’Union confirme ainsi un aspect fondamental de la théorie générale de la présomption relatif à la genèse de celle-ci : elle apparaît là où il y a un doute qu’il convient d’éliminer, au moins jusqu’à la production d’une preuve contraire. La nécessité qu’un tel doute soit écarté peut être identifiée a priori (ce qui doit être présumé) ou a posteriori (ce qu’il est permis de présumer), à l’issue des recherches des preuves de certains faits. En ce sens, le droit de l’Union européenne connaît des présomptions qui font office de preuves aprioriques ou prima facie telles que les présomptions tirées du droit international des traités et des organisations internationales, la légalité, la validité, la conformité et l’équivalence des législations, au sens du principe de reconnaissance mutuelle. En revanche, l’on trouve des faits qui peuvent être présumés dans le droit de la concurrence et les relations extérieures de l’Union, dans l’examen des entraves aux libertés de circulation ainsi que dans l’interprétation des traités. Il peut ainsi être soutenu que le droit de l’Union européenne dispose, matériellement, d’un droit des présomptions qui contient ses propres critères liés à la classification et aux effets probatoires de ces dernières. / It is traditionally held that even though it cannot be qualified as evidence per se, presumption can provisionally produce the effect of evidence, when direct evidence is not available, or even possible, of a fact for which such evidence is required. Considering that the EU does not have a codified law on evidence, the criteria known in national law by virtue of which presumptions are either refutable or irrefutable cannot, prima facie, apply in EU law. This does not mean that the notion of presumption has no place in EU legal vocabulary. The analysis of the case law of the EU Courts, as well as of EU secondary law, allows the discerning of the circumstance in which the legislator, or the judge, use presumptions as techniques that provide good, although temporary, solutions to situations characterized by doubt. The practice in EU law thus confirms a crucial point that has been raised in legal theory on evidence: presumption appears where there is a need to eliminate a doubt, through accepting something to be true until the contrary is established. The need that a doubt be removed can arise a priori (what should be presumed) or a posteriori (what can be presumed), when a search for evidence fails to meet a legal standard. There are, indeed, certain facts that should prima facie be held as true in EU law, such as those given by the presumptions taken over from International law of treaties and of International Organizations, the presumptions of legality and validity, of compliance or compatibility and of equivalence within the meaning of the principle of mutual recognition. The facts that can be presumed in EU law are usually facts for which evidence is required in Competition law, the EU external relations, the restrictions on the freedoms of movement and the interpretation of the Treaties. It can thus be held that there is, in the EU, a law on presumptions, which contains its own criteria related to the division of presumptions, as well as to their evidentiary effects.

Le droit du travail a connu au cours de ces trente dernières années des évolutions remarquables avec, d’une part, l’apparition de nouvelles technologies de l’information et de la communication au sein des entreprises et, d’autre part, l’émergence de l’exigence de justification. Alors que les employeurs sont désormais tenus d’énoncer leurs raisons d’agir et que les salariés travaillent sur des postes informatisés, se pose la question de savoir dans quelle mesure ces nouvelles caractéristiques du monde du travail ont modifié les règles de preuve applicables en la matière. Si la charge de la preuve ne paraît pas avoir été affectée par ces différentes évolutions, il en va différemment de l’objet de la preuve. En effet, l’apparition des toutes dernières technologies de l’information et de la communication participe, au-delà des apparences, à un déplacement de l’objet de la preuve, les salariés ayant désormais accès à de nouveaux éléments de preuve susceptibles d’emporter la conviction des juges. Par ailleurs, l’exigence de justification invite les juges à contrôler plus avant la décision des employeurs. Ces derniers doivent en effet désormais expliciter leurs raisons d’agir. Cela signifie concrètement qu’ils ne peuvent se contenter d’invoquer des faits objectifs, ils doivent encore convaincre les juges de la justesse de leurs décisions en détaillant les ressorts de ces dernières. Ainsi, alors que la doctrine classique avait pour habitude d’affirmer que l’offre de preuve attendue des plaideurs porte sur des faits pertinents, contestés et contestables, l’exigence de justification nous amène à ajouter des faits « contextués », c’est-à-dire des faits articulés au sein d’un discours cohérent et si nous avions pu penser dans un premier temps que l’émergence de l’exigence de justification se traduise par une part croissante de subjectivité dans les décisions de justice, force est de reconnaître au contraire que le contrôle des juges s’est renforcé / The labor law knew during these last thirty years remarkable evolutions with the appearance of new information technologies and communication in the companies and, the creation of “justification’s requirement”. In the mean time employers are now obliged to detail the motivations of their actions and the employees are working more and more on informatics work station. It’s important to understand how these new characteristics have modified the application of the rules of the proof. If the proof’s burden seems to not have been affected by these evolutions, it is not the same about the proof’s object. Indeed, beyond the appearances, the new information and communication technologies lead to a modification of the proof object by giving to the employees the access of new elements of proof susceptible to influence the judge’s conviction. Besides, the “justification’s requirement” invites the judges to better control the employer’s decision. They have now the obligation to clarify their reasons for action. Concretely it means that, to support their claims, they can’t just argue objective facts to convince the judge but they have to justify the logic of their decisions. So, while the classic doctrine had for practice to expect relevant, controversial and questionable facts as proof objects, the “justification’s requirement” brings us to add “sensible facts" (facts articulated within a coherent speech). If at the first time, we could think that the “justification’s requirement” emergence will lead to subjective decision, we are obliged to admit the reinforcement of the judge control.

Résumé: Les propriétés que l'on souhaite exprimer sur les applications système d'information ne peuvent se restreindre aux propriétés statiques, dites propriétés d'invariance, qui portent sur des états du système pris au même moment. En effet, certaines propriétés, dites propriétés dynamiques, peuvent faire référence à l'état passé ou futur du système. Les travaux existants sur la vérification de telles propriétés utilisent généralement le model checking dont l'efficacité pour le domaine des systèmes d'information est plutôt réduite à cause de l'explosion combinatoire de l'espace des états. Aussi, les techniques, fondées sur la preuve, requièrent des connaissances assez avancées en termes de raisonnement mathématique et sont donc difficiles à mettre en œuvre d'autant plus que ces dernières ne sont pas outillées. Pour pallier ces limites, nous proposons dans cette thèse des méthodes de vérification de propriétés dynamiques basées sur la preuve en utilisant la méthode formelle B. Nous nous intéressons principalement aux propriétés d'atteignabilité et de précédence pour lesquelles nous avons défini des méthodes de génération d'obligations de preuve permettant de les prouver. Une propriété d'atteignabilité permet d'exprimer qu'il existe au moins une exécution du système qui permet d'atteindre un état cible à partir d'un état initial donné. Par contre, la propriété de précédence permet de s'assurer qu'un état donné du système est toujours précédé par un autre état. Afin de rendre ces différentes approches opérationnelles, nous avons développé un outil support qui permet de décharger l'utilisateur de la tâche de génération d'obligations de preuve qui peut être longue et fastidieuse.||Abstract: The properties that we would like to express on data-intensive applications cannot be limited to static properties, called invariance properties , that depend on states taken at the same time. Indeed, some properties, called dynamic properties, may refer to the past or the future states of the system. Existing work on the verification of such properties typically use model checking whose effectiveness for data-intensive applications is rather limited due to the combinatorial explosion of the state space. In addition, the techniques, based on the proof, require fairly advanced knowledge and mathematical reasoning especially that they are not always supported by tools. To overcome these limitations, we propose in this thesis proof-based verification approaches that use the B formal method. We are mainly interested in reachability and precedence properties for which we defined formal rules to generate proof obligations that permit to discharge them. A reachability property expresses that there is at least one execution scenario that permits to reach a target state from a given initial state while a precedence property ensures that a given system state is always preceded by another state. To make these different approaches workable, we have developed a support tool that permits to discharge the users from tedious and error-prone tasks.

Le temps de la décroissance de l'activité radioactive de certains radionucléides contenus dans les déchets nucléaires, en dessous d'un seuil considéré comme acceptable, se compte parfois jusqu'en centaines de milliers d'années. Comment les salarié.es de l'Agence Nationale pour la gestion des Déchets Radioactifs (Andra) montrent la sûreté d'un dépôt géologique de ces déchets sur de telles temporalités ? C'est à cette question qu'entreprend de répondre cette thèse, à partir d'une étude des archives de cette agence et d'observation menées au sein de celle-ci.Cette thèse est d'abord une histoire sociale des pratiques savantes mobilisées, depuis les années 1980 jusqu'à 2013, pour étudier l'évolution d'un stockage (géologie, étude des matériaux, simulation numérique...) Elle analyse également le rôle de la recherche dans le gouvernement de l'aval du cycle nucléaire depuis la loi de 1991 qui, en France, encadre la gestion des déchets nucléaires.Bien que l'évacuation géologique soit la seule solution de gestion envisagée pour les déchets radioactifs, la dissociation entre les recherches menées dans le laboratoire souterrain de Bure et leur finalité a permis à l'Andra de s'implanter localement. Cependant, l'Andra se heurte à l'impossibilité épistémique d'appréhender exhaustivement l'évolution d'un stockage sur des centaines de milliers d'années. Désormais, les recherches accompagnent l'implantation du stockage, transformant sans cesse la compréhension de son comportement. Alors que la démonstration publique de la sûreté d'un stockage devient une condition d'acceptation d'un tel ouvrage, l'Andra abandonne peu à peu la prétention à produire une preuve formelle sur le modèle d'une démonstration mathématique : à partir des années 2000, la sûreté repose sur un « faisceau d'arguments » apportant la garantie d'une certaine maîtrise de l'évolution du stockage. Enfin, cette thèse montre au prix de quelles hypothèses la gestion des déchets nucléaires a été promue, durant les années 2000, comme un exemple parfait de démocratie technique. / It takes up to hundreds of thousands of years for the radioactivity contained in some nuclear waste to decrease under acceptable threshold. How engineers and scientists from the French agency for nuclear waste management (Andra) prove the safety of an underground disposal on such a temporality? Based on the study of the Andra's archives and on internal observation, this thesis intends to address and answer the above question.This thesis is first and foremost a social history of scientific practices used to study the evolution of storage (geology, materials science, numerical simulation...) between the 1980’s and 2013. It's also a study of the role of research in governing the back end of the nuclear fuel cycle, after the French law of 1991 provided nuclear waste management with legal framework. Burying nuclear waste is the only option to manage them. However, the distinction between the research undertaken in Bure underground laboratory and their purpose, has allowed Andra's siting. Engineers and scientists from this agency are faced with the epistemic inability to understand exhaustively the evolution of storage during hundreds of thousands years. The progress of the project and researches work jointly and the pursuit of science constantly disrupts the understanding of the storage evolution. When, in the 1990s, the public demonstration of storage safety became a condition of its acceptance, the Andra progressively gave up the idea that a formal demonstration, like a mathematical one, could be produced. Since the 2000s, the storage safety has been based on a “cluster of arguments” which ensures a degree of control over the deposit evolution. Finally, this thesis shows how the French nuclear waste management has been promoted as a prime example of technical democracy.