De plus en plus de calculs de surveillance, contrôle etc. sont effectués de façon logicielle. Notre objectif est de prouver formellement des calculs numériques qui offrent déjà un premier niveau de garantie sur leurs résultats, comme des calculs par intervalles, et en particulier des calculs avec des modèles de Taylor.<br /><br />Cette thèse présente la construction d'une bibliothèque de modèles de Taylor pour l'assistant de preuves PVS. Nous avons développé les modèles de Taylor pour les opérations d'addition, soustraction, multiplication par un scalaire, multiplication, élévation au carré, puissance et racine carrée. Nous avons également développé les modèles de Taylor pour l'exponentielle, le sinus, l'arctangente et les sinus et cosinus hyperboliques. Nous avons démontré dans PVS que les opérations et fonctions définies dans notre bibliothèque préservent la propriété d'inclusion, travail de preuve qui n'avait pas été fait auparavant dans les implantations des modèles de Taylor.<br /><br />Nous avons développé une stratégie PVS pour certifier des inégalités ou bornes d'expressions. Quand on utilise un assistant de preuves pour démontrer une inégalité, il peut être nécessaire de guider l'assistant pas à pas dans la démonstration. Pour cette raison, les utilisateurs effectuent rarement la démonstration. Par conséquent, simplifier la façon de prouver les inégalités et bornes d'expressions facilite l'utilisation de PVS.<br /><br />Notre bibliothèque peut être utilisée pour construire des modèles de Taylor pour des expressions données, pour dériver des bornes plus ou moins précises pour des expressions arithmétiques et également pour certifier des inégalités ou bornes d'expressions. Disposer d'une méthode pour vérifier des expressions dans un assistant de preuves permet de vérifier certaines expressions qui apparaissent dans des logiciels de missions critiques.<br /><br />Pour résumer, nous avons développé une bibliothèque de modèles de Taylor en PVS qui comprend les opérations arithmétiques et certaines fonctions élémentaires. Nous avons démontré la propriété d'inclusion pour les opérations et fonctions développées. Nous avons développé une stratégie appelée containment pour démontrer la propriété d'inclusion des modèles de Taylor construits à partir des opérations et fonctions précédemment définies. Nous avons développé une stratégie appelée taylors pour prouver des inégalités en utilisant les modèles de Taylor. Nous avons illustré sur deux applications l'intérêt de ces développements.

Cette thèse porte sur l'étude théorique et pratique d'un système de typage appliqué à la preuve de programmes de style fonctionnels. Le système de base est le système ST créé par C.Raffalli; il comporte, outre le polymorphisme, du sous-typage et de l'omission de contenu non-algorithmique. Nous étudions tout d'abord les modèles de la théorie définie par le système de types, en construisant une axiomatique basée sur les treillis permettant de modéliser le calcul et la logique. Nous étudions sur cette base le système de types, montrons la réduction du sujet, et la possibilité de définir en interne la normalisabilité et la réductibilité des programmes. Dans la suite de la thèse, plus appliquée, nous étudions des codages de types de données riches inspirés des langages fonctionnels - y incluant notamment un système de modules du premier ordre- dans le Lambda-Calcul, et montrons qu'ils s'intègrent harmonieusement dans le système; la méthodologie développée dans cette partie permet d'étendre le langage de types et le langage de programmation en conservant un critère de consistance assurant la sûreté du code typé.

Au coeur des liens entre Théorie de la Démonstration et Théorie des Types, la correspondance de Curry-Howard fournit des termes de preuves aux aspects calculatoires et équipés de théories équationnelles, i.e. des notions de normalisation et d'équivalence. Cette thèse contribue à étendre son cadre à des formalismes (comme le calcul des séquents) appropriés à des considérations d'ordre logique comme la recherche de preuve, à des systèmes expressifs dépassant la logique propositionnelle comme des théories des types, et aux raisonnements classiques plutôt qu'intuitionistes.<br />La première partie est intitulée Termes de Preuve pour la Logique Intuitioniste Implicationnelle, avec des contributions en déduction naturelle et calcul des séquents, normalisation et élimination des coupures, sémantiques en appel par nom et par valeur. En particulier elle introduit des calculs de termes de preuve pour le calcul des séquents depth-bounded G4 et la déduction naturelle multiplicative. Cette dernière donne lieu à un calcul de substitutions explicites avec affaiblissements et contractions, qui raffine la beta-réduction.<br />La deuxième partie, intitulée Théorie des Types en Calcul des Séquents, développe une théorie des Pure Type Sequent Calculi, équivalents aux Systèmes de Types Purs mais mieux adaptés à la recherche de preuve.<br />La troisième partie, intitulée Vers la Logique Classique, étudie des approches à la Théorie des Types classique. Elle développe un calcul des séquents pour une version classique du Système Fomega. Une approche à la question de l'équivalence de preuves classiques consiste à calculer les représentants canoniques de preuves équivalentes dans le cadre du Calcul des Structures.

Texte remanié de : Thèse de doctorat : Droit : Nice : 2001. / Bibliogr. p. [407]-437. Index.

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

L'arbitrage est un mode de résolution des litiges par l'intermédiaire d'un tribunal arbitral composé d'un ou plusieurs arbitres. Il permet, comme devant les tribunaux étatiques, de régler un litige en vertu d'une sentence rendue à l'issue d'une procédure arbitrale dans laquelle chacune des parties doit prouver ce qu'elle allègue afin d'établir la conviction des arbitres. C'est par le recours aux divers modes de preuve inspirés des différents systèmes juridiques notamment du système de Common Law et du système de droit civil que les plaideurs pourront atteindre cette finalité.En revanche, parce que l'arbitrage international ne possède ni for ni législation spéciaux, l'administration des preuves dans une instance arbitrale internationale revêt un caractère sui generis de fait que l'arbitrage international a reconnu un système de preuve qui a utilisé les avantages des divers systèmes juridiques. Ainsi, on retrouve que la preuve écrite, qu'elle soit sur support papier ou sur support électronique, est administrée selon le model civiliste qui donne la primauté à une preuve préconstituée à l'avance. Mais, en ce qui concerne la preuve par témoin, l'influence des droits de Common Law paraît claire surtout que dans la plupart des cas, le pouvoir de nommer et d'interroger les témoins revient aux plaideurs qui utilisent la méthode d'Examination lors de l'interrogation des témoins. C'est aussi le cas de l'expertise qui est souvent considérée comme une preuve orale dans laquelle il revient aux parties le pouvoir de désigner les experts et de les interroger suivant l'interrogatoire direct et le contre interrogatoire tout comme des témoins. Ainsi, les preuves dans l'arbitrage international peuvent être reparties en preuves écrites et preuves orales dont les premières sont constituées de l'écrit sur support papier ou sur support électronique et les secondes sont formées par la preuve par témoin et la preuve par expertise.

Cette thèse présente une coopération entre l'assistant de preuve Coq et certains prouveurs externes basée sur l'utilisation de traces de preuves. Nous étudions plus particulièrement deux types de prouveurs pouvant renvoyer des certicats : d'une part, les réponses des prouveurs SAT et SMT peuvent être vériées en Coq afin d'augmenter à la fois la confiance qu'on peut leur porter et l'automatisation de Coq ; d'autre part, les théorèmes établis dans des assistants de preuves basés sur la Logique d'Ordre Supérieur peuvent être exportés en Coq et re-vérifiés, ce qui permet d'établir des preuves formelles mêlant ces deux paradigmes logiques. Cette étude a abouti à deux logiciels : SMTCoq, une coopération bi-directionnelle entre Coq et des prouveurs SAT/SMT, et HOLLIGHTCOQ, un outil important les théorèmes de HOL Light en Coq. L'architecture de chacun de ces deux développements a été pensée de manière modulaire et efficace, en établissant une séparation claire entre trois composants: un encodage en Coq du formalisme de l'outil externe qui est ensuite traduit avec soin vers des termes Coq, un vérificateur certifié pour établir les preuves, et un pré-processeur écrit en Ocaml traduisant les traces venant de prouveurs différents dans le même format de certicat. Grâce à cette séparation, un changement dans le format de traces n'affecte que le pré-processeur, sans qu'il soit besoin de modier du code ou des preuves Coq. Un autre composant essentiel pour l'efficacité et la modularité est la réflexion calculatoire, qui utilise les capacités de calcul de Coq pour établir des preuves à la fois courtes et génériques à partir des certificats.

En ajoutant au lambda-calcul des structures de données algébriques, des types dépendants et un système de modules, on obtient un langage de programmation avec peu de primitives mais une très grande expressivité. L'assistant de preuve Coq s'appuie sur un tel langage (le CIC) à la sémantique particulièrement claire. L'utilisateur n'écrit pas directement de programme en CIC car cela est ardu et fastidieux. Coq propose un environnement de programmation qui facilite la tâche en permettant d'écrire des programmes incrémentalement grâce à des constructions de haut niveau plus concises. Typiquement, les types dépendants imposent des contraintes fortes sur les données. Une analyse de cas peut n'avoir à traiter qu'un sous-ensemble des constructeurs d'un type algébrique, les autres étant impossibles par typage. Le type attendu dans chacun des cas varie en fonction du constructeur considéré. L'impossibilité de cas et les transformations de type doivent être explicitement écrites dans les termes de Coq. Pourtant, ce traitement est mécanisable et cette thèse décrit un algorithme pour réaliser cette automatisation. Par ailleurs, il est nécessaire à l'interaction avec l'utilisateur de calculer des programmes du CIC sans faire exploser la taille syntaxique de la forme réduite. Cette thèse présente une machine abstraite conçu dans ce but. Enfin, les points fixes permettent une manipulation aisée des structure de données récursives. En contrepartie, il faut s'assurer que leur exécution termine systématiquement. Cette question sensible fait l'objet du dernier chapitre de cette thèse.

Cette note de synthèse pour une Habilitation à Diriger des Recherches présente une modélisation épistémologique de l'activité de définition en mathématiques, en explicitant la dialectique entre définition et preuve. Et cela, bien sûr, dans une perspective didactique, en vue de concevoir, analyser et transmettre des situations de construction de définitions. La première partie présente l'objet d'étude et la méthodologie. Une analyse critique des travaux de recherche internationaux en didactique sur l'étude l'activité de définition en mathématiques est présentée en deuxième partie. Sont soulignés en particulier les points de convergence et de tension, ainsi que les manques - épistémologiques et didactiques - sur la question. La troisième partie présente une modélisation épistémologique de référence de l'activité de définition en mathématiques, activité en dialectique avec la preuve, en prenant appui sur des expérimentations (niveaux secondaire et supérieur), et des entretiens avec des mathématiciens. Différents cadres théoriques issus de la didactique des mathématiques et des mathématiques sont sollicités. La quatrième et dernière partie aborde de nouvelles perspectives de recherche à trois niveaux (épistémologique, théorique, et didactique).

L’établissement juridictionnel de la preuve recouvre la recherche, la présentation et l’appréciation des preuves lors d’un procès. Cette étude vise à saisir, s’il existe entre les juges administratif, civil et pénal qui jugent en matière fiscale, une unité dans l’établissement de la preuve. Il s’agit d’une étude de droit comparé interne. A première vue, l’établissement juridictionnel de la preuve est, devant les juges de la matière fiscale, le fruit de procédures différentes qui sont adaptées aux litiges qui leur reviennent de juger. Sous cet angle, chaque juge de la matière fiscale dispose d’un office qui lui est propre. Chaque procédure dispose ainsi d’une identité spécifique qui imprime sur la réalité factuelle un particularisme. La preuve judiciaire dispose ainsi d’un aspect vernaculaire qu’il convient d’identifier. Toutefois, l’établissement juridictionnel de la preuve peut révéler un autre visage. L’affirmation de principes fondamentaux qui conditionnent l’établissement de la preuve atteste qu’au-delà des différentes procédures se dessine une fondamentalité probatoire qui unit les juges administratif, civil et pénal tant en matière fiscale qu’en dehors de ce champ. Ces principes fondamentaux – qui sont ici identifiés – forgent une unité partielle dans l’établissement juridictionnel de la preuve. Sous cette lumière, une conception partagée de la vérité judiciaire s’affirme sur le fondement d’une vision commune de la Justice. / This essay deals with the search, the submission and the evaluation of the evidence in a trial. This work is a comparison between administrative, civil and criminal judge in matter of evidence. At first glance, the fact finding process is based on different procedures and each judge has a proper role. Each procedure has a distinctive identity. However, another face of the fact finding process is being seen. The continued development of fundamental rights transforms the fact finding process. In this light, fact finding process provides a relative unit on the base of a common understanding of Justice.