Cette Thèse est la conclusion de trois ans de travail sur un projet nommé DemoNat. Le but de ce projet est la conception d'un système d'analyse et de vérification de démonstrations mathématiques écrites en langue naturelle.<br><br>L'architecture générale du système se décrit en 4 phases :<br>- analyse de la démonstration par des outils linguistiques ;<br>- traduction de la démonstration dans un langage restreint ;<br>- interprétation du texte traduit en un arbre de règles de déduction ;<br>- validation des règles de déduction à l'aide d'un démonstrateur automatique.<br><br>Ce projet a mobilisé des équipes de linguistes et de logiciens, les deux premières phases étant la tâche des linguistes, et les deux dernières étant la tâche des logiciens.<br><br>Cette thèse présente plus en détail ce projet et développe principalement les points suivants :<br>- définition du langage restreint et de son interprétation ;<br>- propriétés du type principal de termes d'un lambda-calcul typé avec deux flèches entrant dans le cadre d'un outil linguistique, les ACGs ;<br>- description du démonstrateur automatique.

Mes travaux de recherche portent sur la théorie de la démonstration, le lambda-calcul et l'informatique théorique, dans la ligne de la correspondance de Curry-Howard entre les preuves et les programmes.<br /><br />Dans ma thèse de doctorat, j'ai étudié les opérateurs de mise en mémoire pour les types de données. Ces notions, qui sont introduites par Krivine, permettent de programmer en appel par valeur tout en utilisant la stratégie de la réduction de tête pour exécuter les $\lambda$-termes. Pour cette étude, j'ai introduit avec David une extension du $\lambda$-calcul avec substitutions explicites appelée $\lambda$-calcul dirigé. Nous en avons déduit une nouvelle caractérisation des termes de mise en mémoire et obtenu des nombreux résultats très fins à leur sujet. En ce qui concerne le typage des opérateurs de mise en mémoire, Krivine a trouvé une formule du second ordre, utilisant la non-non traduction de Gödel de la logique classique dans la logique intuitionniste, qui caractérise ces opérateurs. Je me suis attaché à diverses généralisations du résultat de Krivine pour les types à quantificateur positif dans des extensions de la logique des prédicats du second ordre.<br /><br />J'ai poursuivi, après ma thèse, une activité de recherche sur l'extension de la correspondance de Curry-Howard à la logique classique, au moyen des instructions de contrôle. J'ai étudié des problèmes liés aux types de données dans deux de ces systèmes : le $\lambda \mu$-calcul de Parigot et le $\lambda C$-calcul de Krivine. J'ai donné des algorithmes très simples permettant de calculer la valeur d'un entier classique dans ces deux systèmes. J'ai également caractérisé les termes dont le type est l'une des règles de l'absurde. J'ai étendu le système de Parigot pour en obtenir une version non déterministe mais où les entiers se réduisent toujours en entiers de Church. Curieusement, ce système permet de programmer la fonction ``ou parallèle''.<br /><br />Je me suis intéressé aux systèmes numériques qui servent à représenter les entiers naturels au sein du $\lambda$-calcul. J'ai montré que pour un tel système, la possession d'un successeur, d'un prédécesseur et d'un test à zéro sont des propriétés indépendantes, puis qu'un système ayant ces trois fonctions possède toujours un opérateur de mise en mémoire. Dans un cadre typé, j'ai apporté une réponse négative à une conjecture de Tronci qui énonçait une réciproque du résultat précédent.<br /><br />La notion de mise en mémoire ne s'applique qu'à des types de données. Une définition syntaxique a été donné par Böhm et Berarducci, et Krivine a proposé une définition sémantique de ces types. J'ai obtenu avec Farkh des résultats reliant la syntaxe et la sémantique des types de données. Nous avons proposé également des définitions des types entrée et des types sortie pour lesquelles nous avons montré diverses propriétés syntaxiques et sémantiques.<br /><br />J'ai réussi à combiner la logique intuitionniste et la logique classique en une logique mixte. Dans cette logique, on distingue deux genres de variables du second ordre, suivant que l'on peut, ou non, leur appliquer le raisonnement par l'absurde. Ce cadre m'a permi de donner le type le plus général pour les opérateurs de mise en mémoire. Vu le rôle important que cette logique semble devoir jouer dans la théorie de ces opérateurs, j'en ai mené avec A. Nour une étude théorique approfondie. Le système de logique mixte propositionnelle auquelle nous avons abouti évoque les sytèmes $LC$ de Girard et $LK^{tq}$ de Danos, Joinet et Schellinx.<br /><br />Je me suis intéressé avec David à l'équivalence induite par l'égalité entre les arbres de Böhm infiniment $\eta$-expansés. Avec Raffalli, je me suis également intéressé à la sémantique de la logique du second ordre.

La facilité compte parmi les notions les plus fines de l'indéfini en lambda-calcul. Un terme est dit facile s'il peut être identifié à tout autre terme clos arbitraire sans soulever de contradiction. Introduite en 1975 par Jacopini, elle fait depuis l'objet de recherches qui visent à caractériser la forme des termes faciles. Aujourd'hui, de tous les travaux entrepris il se dégage qu'un tel terme doit posséder une périodicité. Être périodique, c'est être équivalent à un sous-terme propre de l'un de ses réduits. Ici, la périodicité apparaîtra sous les traits de l'auto-similarité. Sont auto-similaires les termes dont l'arbre de Berarducci réapparaît comme sous-arbre propre à lui-même. La facilité de tels termes demeure un mystère. À ce jour, nous n'en connaissons que peu d'exemples. Le terme "Y omega_3" constitue un exemple typique dont la question de la facilité reste ouverte. Dans cette thèse, nous étendrons la connaissance de l'ensemble des termes m identiables à Y Omega_3. Nous montrerons que dans un cas critique où lambda-beta +{Y Omega_3 = m} implique m = delta_3, sous certaines hypothèses, m est lui-même auto-similaire. Ils s'en suit une description possible de toutes les équations dérivées de {Y Omega_3= m} sous la forme de classes confinantes.

Dans cette thèse nous avons étudié certaines questions mathématiques associées au calcul de l'action spectrale de Chamseddine--Connes sur des exemples fondamentaux de triplets spectraux non commutatifs, tels que le tore non commutatif et la 3-sphère quantique SUq(2). Nous avons montré en particulier qu'une condition diophantienne sur la matrice de déformation du tore est cruciale pour obtenir l'action spectrale en tenant compte de la structure réelle. <br />Nous avons aussi étudié la question de l'existence de tadpoles (termes linéaires par rapport au potentiel de jauge de la fluctuation de la métrique dans l'action spectrale) dans le cas de géométries riemanniennes commutatives, et la construction d'un calcul pseudodifférentiel global permettant une généralisation du produit de Weyl--Moyal sur un espace de Schwartz de sections rapidement décroissantes sur un fibré cotangent d'une variété avec linéarisation.

Le fil conducteur est celui des conditions de compatibilité des systèmes aux dérivées partielles de la Mécanique des Solides Déformables. L'idée initiale, présentée dans l'ouvrage de Gaston Darboux sur la théorie générale des surfaces, est reprise. Elle consiste à remplacer les symboles de Christoffel par des vecteurs appelés vecteurs de Darboux. Ces vecteurs sont associés à des rotations de la même manière qu'un vecteur rotation instantanée est mis en évidence lors de l'étude du mouvement d'un solide rigide. <br />Les conditions de compatibilité en grandes déformations sont ainsi revisitées à la Darboux. Deux systèmes aux dérivées partielles découplés permettent d'obtenir le déplacement du milieu déformé en deux intégrations successives. L'étude de la nature tensorielle des objets exhibés montre la validité de nos concepts. Une étude inédite des variétés riemanniennes de dimension 3 de même courbure que la sphère est développée. De même, la théorie des surfaces est revue en introduisant les vecteurs de Darboux. La reconstruction d'une surface connaissant ses deux formes fondamentales est proposée conformément au théorème de Bonnet. L'étude particulière d'une surface minimale conduit à un processus de construction effectif à partir de la connaissance du bord. La notion de surface minimale sœur est dégagée, deux exemples sont présentés. Enfin l'équivalence entre l'annulation du tenseur de courbure de Riemann-Christoffel dans une coque et les conditions de Gauss-Codazzi-Mainardi sur sa surface moyenne est établie. Des perspectives, regardant le solide rigide comme une variété riemannienne de dimension 6, sont évoquées.

La facilité compte parmi les notions les plus fines de l'indéfini en λ-calcul. Un terme est dit facile s'il peut être identifié à tout autre terme clos arbitraire sans soulever de contradiction. Introduite en 1975 par Jacopini, elle fait depuis l'objet de recherches qui visent à caractériser la forme des termes faciles. Aujourd'hui, de tous les travaux entrepris il se dégage qu'un tel terme doit posséder une périodicité i.e être β-équivalent à un sous-terme propre de l'un de ses réduits. Ici, la périodicité apparaîtra sous les traits de l'auto-similarité. Sont auto-similaires les termes dont l'arbre de Berarducci réapparaît comme sous-arbre propre à lui-même. La facilité de tels termes demeure un mystère et à ce jour, nous n'en connaissons que peu d'exemples. Le terme Yt Ω3 constitue un exemple typique dont la question de la facilité reste ouverte. Dans cette thèse, nous élargirons la connaissance de l'ensemble des termes m identifiables à Yt Ω3. Nous montrerons que dans un cas critique où λβ +{Yt Ω3 = m} |- m = δ3, sous certaines hypothèses, m est lui-même auto-similaire. Ils s'en suit une description possible de toutes les équations dérivées de {Yt Ω3 = m} sous la forme de classes confinantes.

Ce mémoire est composé de deux grandes parties. Dans la première, nous simulons le fonctionnement d'automates cellulaires par différents modèles de calcul parallèle comme les PRAM, les XPRAM et les machines spatiales. Nous obtenons ainsi différentes preuves de l'universalité de ces modèles. Nous tirons quelques conséquences de ces résultats du point de vue de la calculabilité et de la complexité. Dans la seconde partie, nous considérons les automates cellulaires définis sur des graphes de Cayley finis. Nous rappelons la simulation de Róka qui permet de mimer le fonctionnement d'un tore hexagonal d'automates par un tore d'automates de dimension deux. Nous décrivons ensuite différentes manières de plonger un tore d'automates de dimension deux dans un anneau d'automates. Nous déduisons de ces résultats la simulation de tores de dimension finie par un anneau d'automates et celle d'un tore hexagonal d'automates par un anneau d'automates.

La mutualisation des ressources physiques réparties dans les universités, les instituts et les entreprises a permis l'émergence des grilles de calcul. Ces infrastructures dynamiques sont bien adaptées aux applications scientifiques ayant de grands besoins en puissance de calcul et en espace de stockage. L'un des défis majeur pour les grilles de calcul reste la simplification de leur utilisation. Contrairement au déploiement d'applications sur une infrastructure centralisée, le déploiement sur une grille nécessite de nombreuses tâches pénibles pour l'utilisateur. La sélection des ressources, le transfert des programmes ainsi que la surveillance de l'exécution sont en effet laissés à sa charge. Aujourd'hui, de nombreux travaux proposent d'automatiser ces étapes dans des cas simples. En revanche très peu permettent de prendre en charge des déploiements plus complexes, comme par exemple le redéploiement d'une partie de l'application pendant son exécution ou encore le déploiement coordonné de plusieurs applications. <br /><br />Dans cette thèse, nous proposons un modèle pour prendre en charge le déploiement dynamique des applications sur les grilles de calcul. Ce modèle vise à offrir deux fonctionnalités principales. La première consiste en la traduction d'actions de haut niveau, spécifiques aux applications, en opérations de bas niveau, relatives à la gestion des ressources sur la grille. La deuxième consiste en la pré-planification des déploiements, redéploiements et codéploiements d'applications sur les ressources physiques. <br /><br />Le modèle satisfait trois propriétés. Il rend transparent la gestion des ressources à l'utilisateur. Il offre des actions spécifiques aux besoins de l'application. Enfin, il est non-intrusif en limitant les contraintes sur le modèle de programmation de l'application. <br /><br />Une proposition d'architecture nommée CORDAGE vient illustrer ce modèle pour le co-déploiement et le redéploiement d'applications. CORDAGE a été développé en lien avec l'outil de réservation OAR et l'outil de déploiement ADAGE. La validation du prototype s'est effectuée avec la plate-forme pair-à-pair JXTA, le service de partage de données JUXMEM ainsi que le système de fichiers distribué GFARM. Notre approche a été évaluée sur la grille expérimentale GRID' 5000.<br /><br />http://cordage.gforge.inria.fr/

Le but de cette thèse est la construction d'une méthode de calcul effectif des multiplicateurs de Stokes avec évaluation de l'erreur. Cette méthode s'applique à tous les systèmes de niveau unique et au premier niveau des systèmes de niveaux multiples. Dans une partie théorique, nous commençons par établir la résurgence des solutions formelles en suivant la méthode d'Ecalle par perturbation régulière et séries majorantes. Nous déduisons de celle-ci une description précise des singularités dans le plan de Borel en déterminant les coefficients de résurgence et les multiplicateurs de Stokes. Dans la partie numérique, nous supposons que les systèmes sont à coefficients rationnels et nous choisissons de travailler dans le plan de Borel en calculant les coefficients de résurgence par prolongements analytiques successifs. En particulier, nous construisons des algorithmes permettant d'évaluer l'erreur. Nous illustrons également cette méthode de calcul par plusieurs exemples numériques.

L'objectif de cette thèse est d'explorer des descriptions formelles pour la structure et le fonctionnement des systèmes biologiques, ainsi que des outils formels pour raisonner au sujet de leur comportement. Cette thèse s'inscrit dans les travaux étudiant les modèles informatiques sûrs où les calculs sont exprimés par l'intermédiaire de la réécriture, et où nous pouvons compter sur la vérification formelle pour exprimer et valider les propriétés des modèles. Dans cette thèse nous développons un calcul de réécriture d'ordre supérieur pour décrire des molécules, des règles de réaction, et la génération des réseaux biochimiques. Le calcul est basé sur la métaphore chimique en décrivant les calculs en termes de solutions chimiques dans lesquelles les molécules représentant des données agissent l'une sur l'autre librement selon des règles de réaction. Ainsi nous avons obtenu un Calcul Biochimique Abstrait étendant le modèle chimique d'ordre supérieur en considérant des molécules structurées. Le calcul est équipé d'une spécification naturelle de la concurrence et des mécanismes de contrôle grâce à l'expression des stratégies de réécriture sous forme de molécules. La description des complexes moléculaires ou des réactifs chimiques appartient à une classe spécifique de graphes. Nous définissons la structure des graphes avec ports et nous montrons que les principes du calcul biochimique instanciés pour les graphes avec ports sont assez expressifs pour modéliser des systèmes autonomes et des réseaux biochimiques. En plus, les techniques de la réécriture stratégique ouvrent la voie au raisonnement basé sur les calculs et à la vérification des propriétés des systèmes modélisés.