On verra comment la positivité de certains opérateurs sur une surface riemannienne permet d'obtenir des informations sur le type conforme de la surface. Ce type de résultat trouve son origine dans l'étude des surfaces minimales stables.
La théorie des jeux peut être vue comme la théorie des équilibres. Comme elle est un peu plus que cinquantenaire, il peut sembler opportun de la réexaminer. C'est ce que nous faisons en proposant une nouvelle vision plus générale que nous appelons 171jeux à conversion-préférence187, en abrégé 171jeux CP187. Ce formalisme semble s'adapter agréablement aux réseaux de régulation de gênes.
Travail en commun avec D. Cohen-Steiner (INRIA Sophia-Antipolis) et A. Lieutier (Dassault Systèmes). Dans cet exposé, nous aborderons la question de la ``stabilité de la topologie'' des sous-ensembles compacts de R^n par perturbation pour la distance de Hausdorff : étant donné deux compacts K et K' dont la distance de Hausdorff est petite, peut-on déduire la topologie de K de celle de K'? En toute généralité, la réponse à cette question est évidemment négative. Cependant, nous verrons que si K appartient a une large classe de compacts (contenant les sous-analytiques), on peut apporter une réponse positive à la question précédente. L'approche adoptée est basée sur quelques propriétés de la fonction distance a un compact que nous rappelerons.
L'estimation et l'approximation de grandeurs topologiques ou géométriques associées à des formes dont on ne connait qu'une approximation posent des problèmes pratiques et théoriques délicats en calcul géométrique. Ces problèmes ont été largement étudiés depuis plusieurs années dans le cas de la reconstruction d'hypersurfaces lisses dans R^n : à partir d'un nuage de points mesurés sur une forme lisse, on souhaite 'reconstruire' la surface de cette forme en garantissant que le résultat produit possède la même topologie que celle de la forme échantillonnée. Il existe bon nombre de résultats et d'algorithmes satisfaisant permettant de répondre a ce problème dans le cas particulier des surfaces dans R^3.Cependant, les résultats et les méthodes actuelles possèdent un double inconvénient. Ils ne se généralisent pas à des objets non lisses et conduisent à des algorithmes inefficaces en dimension supérieure à 3. Le développement récents des outils de mesure et de simulation nécessite de mettre au point des techniques mathématiques et algorithmiques permettant d'extraire l'information topologique et géométrique de nuages de points issus d'objets non lisses dans des espaces de toutes dimensions. Dans cet exposé, nous présenterons quelques résultats récents dans cette voie. Nous verrons en particulier, que dans le cas de l'approximation d'objets non lisses, il apparait des ``phenomènes d'échelle'' faisant apparaitre différentes topologies à différentes échelles.
Model checking is a successful technique for verifying automatically temporal properties of concurrent finite-state programs represented as Labelled Transition Systems (LTSs). Among the various formalisms used for specifying properties, an outstanding candidate is the modal mu-calculus, a very powerful fixed point-based temporal logic. However, in spite of its theoretical expressiveness, standard modal mu-calculus is a too low-level formalism for end-users, making the specification of complex properties tedious and error-prone. In this talk, we propose MCL (Model Checking Language), an extension of the modal mu-calculus with high-level, data-based constructs inspired from programming languages, which substantially increase its expressive power as well as the conciseness and readability of properties. We also present an on-the-fly model checking method for verifying MCL formulas on LTSs, based upon translating the verification problem into the resolution of a boolean equation system. The MCL language and the associated verification method are supported by the EVALUATOR 4.0 model checker, developed within the CADP verification toolbox using the generic OPEN/CAESAR environment for on-the-fly exploration of LTSs.
Parce que les nombres manipulés en machine ont généralement un domaine et une précision limités, il est nécessaire de certifier soigneusement que les applications les utilisant se comportent correctement. Réaliser une telle certification à la main est un travail propice à de nombreuses erreurs. Les méthodes formelles permettent de garantir l'absence de ces erreurs, mais le processus de certification est alors long, fastidieux et généralement réservé à des spécialistes. Le travail présenté dans cet exposé vise à rendre ces méthodes accessibles en automatisant leur application. L'approche adoptée s'appuie sur une arithmétique d'intervalles accompagnée d'une base de théorèmes sur les propriétés des arithmétiques approchées et d'un mécanisme de réécriture d'expressions permettant le calcul de bornes fines sur les erreurs d'arrondi. Ce travail s'est concrétisé par le développement de l'outil Gappa d'aide à la certification. Il permet de vérifier les propriétés de codes numériques qui utilisent de l'arithmétique à virgule fixe ou à virgule flottante. Cette vérification s'accompagne de la génération d'une preuve formelle de ces propriétés utilisable par l'assistant de preuves Coq. Cette preuve s'appuie sur une bibliothèque de propriétés arithmétiques et elle contient principalement des calculs entiers qui reflètent les calculs par intervalles effectués par l'outil. Cependant, pour que la preuve soit d'une taille raisonnable, Gappa élimine les lemmes inutiles et simplifie les nombres que Coq aura à manipuler. Gappa a été utilisé avec succès pour certifier la correction de fonctions dans les bibliothèques CRlibm, CGAL et FLIP par exemple.
Nous parlerons de calculabilités généralisées permettant de définir de nouvelles complexités à la Kolmogorov-Chaitin et de préciser les liens entre incomplétude et calcul.
Nous aborderons les récents développements en géométrie énumérative réelle. Combien de courbes algébriques de genre 0 passent par une collection quelconque de points dans le plan P2 ? Une approche actuelle consiste à construire des espaces de modules spécifiques et répondre à cette question par un calcul (co)homologique suivant Kontsevich (en complexe) puis Welschinger (en réel). Dans le cadre réel il est nécessaire de prendre en compte l'orientation de ces espaces et c'est ce point qui sera traité dans la détermination de certaines classes caractéristiques.
Cet exposé s'appuit sur le langage lambdaO (Park, Pfenning et Thrun), un langage fonctionnel typé pur étendu avec une notion de variable aléatoire. C'est un travail commun avec Christine Paulin. Après en avoir donné une présentation succinte, et illustré son pouvoir expressif, nous abordons des aspects sémantiques. Nous en proposons une sémantique dénotationnelle directe, à partir de laquelle nous produisons mécaniquement un système d'inférence pour la sémantique axiomatique à la Hoare. Des exemples de preuves en correction partielle sont proposés ; la correction totale est abordée, mais le cadre formel n'est pas complet à ce jour. Enfin, nous indiquerons comment la vérification d'algorithmes (fonctionnels) probabilistes est envisagée dans la suite de notre travail.
Cet exposé est une petite introduction au livre de Jean-Marie Souriau intitulé << Structure des systèmes dynamiques >> (Dunod, 1970) dans lequel l'auteur propose un nouveau cadre pour traiter de la mécanique lagrangienne, cadre malheureusement trop peu connu, même de nos jours... Cette approche a l'avantage de dépasser les divers formalismes classiquement utilisés en mécanique analytique : espace des configurations, espace des phases, équations d'Euler-Lagrange ou équations de Hamilton. En outre, alors que ces derniers points de vue ne permettent même pas de rendre compte du simple principe de relativité galiléenne et sont donc insatisfaisants, l'approche développée par Jean-Marie Souriau montre comment la géométrie symplectique est à l'oeuvre de façon unificatrice dans des branches aussi variées de la physique telles que la mécanique classique, la mécanique statistique ou encore la mécanique quantique.
Mettre en place une plaforme numérique performante, portable, modulable et conviviale est l'un des objectifs de l'association IBPSA dirigée en France par Etienne Wurtz (DR CNRS, Institut Nationale de l'Energie Solaire). Cette journée a pour but de mettre en lumière divers axes de recherche nécessaires à la mise en place de cette plateforme numérique et faisant appel à la modélisation, à l'étude mathématique théorique et numérique des systèmes obtenus : phénomènes multi-échelles, décomposition de domaines, identification de paramètres, optimisation en sont quelques exemples. La proximité de l'INES avec le Laboratoire de mathématiques de l'Université de Savoie ainsi que la proximité du laboratoire Trèfle avec le laboratoire de Mathématiques de Bordeaux a motivé l'organisation de cette journée entre les deux régions : Aquitaine et Rhône-Alpes. Quelques représentants de Grenoble (LMC-IMAG) et de Lyon1 (Institut Camille Jordan) seront également présents. La page web de la journee INES/LAMA est : http://www.lama.univ-savoie.fr/Journee-LAMA-INES/
En recherchant des résultats sur la suite de Conway et le (fameux ?) théorème cosmologique, Pierre est tombé sur un article pour le moins intrigant du même monsieur. Considérez la suite (ordonnée) de fractions suivante : 17/91 78/85 19/51 23/38 29/33 77/29 95/23 77/19 1/17 11/13 13/11 15/2 1/7 55/1 Partez de l'entier 2 et à chaque étape multipliez l'entier courant par la première fraction pour laquelle le produit est entier et répétez le processus. Vous obtenez la suite des 2^p où les p sont les nombres premiers consécutifs. Un miracle pensez vous ? Non, un simple exemple de programme d'un langage de programmation universel : FRACTRAN.
Libraries are a major instrument of software engineering, making it possible to reuse code and to distribute labour between programmers with different areas of expertise. The sophisticated application programs we have today would not be possible without huge libraries in areas such as data structures, numerical analysis, signal processing, and computer graphics. Grammars of natural languages are a domain of a lot of expert knowledge, which it would be useful to find in software libraries. However, typical implementations of grammars are monolithic application programs, such as parsers tuned to a particular corpus. New applications typically have to build their grammars from scratch, which makes it costly to build programs such as natural-language interfaces, or to perform high-quality software localization. This talk presents an approach where grammars can be used as libraries for new grammars and for programs that involve natural language components. The approach is implemented in GF (Grammatical Framework), which is a special-purpose functional programming language for writing grammars. Several features of GF are used in an essential way: the division between abstract and concrete syntax; the module system, including parametrized modules; the type system, which is able to enforce grammar checking via type checking; and code generation that makes GF grammars usable in other programming languages, such as C, Haskell, and Java. To bring the discussion to concrete level, we introduce the GF Resource Grammar Library, which implements the basic grammars of ten languages and makes them accessible to non-linguist application programmers. As an application, we show how the library can be used in building a natural-language interface to a proof system.
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érication de démonstrations mathématiques écrites en langue naturelle. L'architecture générale du système se décrit en 4 phases : 1. analyse de la démonstration par des outils linguistiques ; 2. traduction de la démonstration dans un langage restreint ; 3. interprétation du texte traduit en un arbre de règles de déduction ; 4. validation des règles de déduction à l'aide d'un démonstrateur automatique. 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. Cette thèse présente plus en détail ce projet et développe principalement les points suivants : - définition du langage restreint et de son interprétation ; - propriétés du type principal de termes d'un lamlbda-calcul typé avec deux flèches entrant dans le cadre d'un outil linguistique, les ACGs ; - description du démonstrateur automatique.
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 développé par C.Raffalli; il comporte, outre le polymorphisme, du sous-typage et de l'omission de contenu algorithmique. Nous étudions tout d'abord les modèles de la théorie définie par le système de types en se basant sur des treillis complets comportant des propriétés additionnelles permettant d'interpréter types et termes;puis nous étudions diverses propriétés théoriques du système telles que la réduction du sujet ainsi que son expressivité à travers des exemples traitant de la possibilité ou de l'impossibilité de définir des notions-clés de la logique et de l'informatique théorique. Dans la suite de la thèse, plus appliquée, nous étudions des codages de types de données riches issus de l'informatique 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é.
On propose une notion de modèle pour la logique intuitionniste, qui étend celle fondée sur les algèbre de Heyting. Cette notion de modèle permet de distinguer l'équivalence logique (si A est démontrable, alors B aussi, et vice-versa) de l'équivalence calculatoire (toute démonstration de A est une démonstration de B, et vice-versa), ce que ne permettaient pas de faire les algèbres de Heyting. On montre ensuite que cette notion de modèle peut être utilisée pour démontrer la normalisation des démonstrations dans de nombreuses théories comme l'arithmétique de Peano ou la logique d'ordre supérieur.
On considérera la distance associée à la norme de Bombieri sur l'ensemble des polynômes homogènes réels de degré d à n variables. On montrera que si le niveau P=0 est lisse et extremal (on ne peut pas ajouter de composante à P=0 sans changer le degré) alors la distance au discriminant réel (l'ensemble des polynomes Q réels avec au moins une singularité réelle) est min{ |P(x)| ; x dans S^{n-1}, x point critique de P} On en déduira une inégalité entre la taille des composantes connexes de P=0 et la distance au discriminant.
JERA (Journées EDP Rhone Alpes) A Saint-Etienne
Le nombre de courbes algébriques complexes nonsingulières de degré d passant par d(d+3)/2 - t points et tangentes à t droites est (2(d-1))^t (si la configuration est générique et t<2d-1). F. Ronga a montré que pour une droite (t=1) le problème réel correspondant était maximal: il existe une configuration générique de points réels et d'une droite réelle telle que 2(d-1) courbes de degré d passent par les points et sont tangentes a la droite. En utilisant la géométrie tropicale on montre la maximalité de ce problème énumératif réel pour deux droites (t=2).
In this talk we present a categorical proof theory for a logic for pragmatics. The aim of this logic is to provide a framework that allows to formalize reasoninig about the pragmatic force with which a sentence may be uttered. The concept of pragmatic force comes from speech act theory and plays a crucial role also in certain branches of artificial intelligence, in particular in the developement of communication protocols for software agents. Instead of considering the full-blown theory of speech acts we focus here on speech acts that either have the pragmatic force of an assertion or the pragmatic force of an obligation, and on how these speech acts can be related to each other. In particular, we are interested in a principle proposed by Bellin and Dalla Pozza that allows the propagation of obligations through causal chains of assertions. The study of such principles from the point of view of categorical proof theory is a nontrivial task and we discuss some of the issues that need to be considered in order to get soundness and completeness results.