On présente une extension du lambda-bar-mu calcul de Herbelin avec une opération binaire sur les piles (ou contextes), qui peut aussi être interprétée comme un opérateur de choix non déterministe. Les règles de réduction associées dotent cette opération de propriétés similaires à celles du produit de convolution sur les distributions. C'est la version lambda-calculesque d'une extension par polarisation des réseaux d'interaction différentiels d'Ehrhard-Régnier: on met ce fait en évidence grâce à une sémantique dénotationnelle dans la catégorie des ensembles et relations.
De nombreux travaux d'océanographes ont montré la validité des équations de Saint-Venant pour la description des phénomènes associés aux vagues dans la ``zone de surf''. En particulier, la théorie hyperbolique permet de bien décrire les phénomènes de dissipation d'énergie au travers des fronts d'ondes (chocs). Concernant la simulation numérique de ces phénomènes, certains points restent délicats, en particulier la simulation des phénomènes de découvrement/recouvrement que l'on observe sur la plage. Dans cette optique, un nouveau modèle numérique est présenté ici, associant solveur de Riemann approché de type VFRoe, préservant la positivité, et approche well-balanced pour prendre en compte les termes sources. Une extension vers un schéma well-balanced d'ordre élevé permettant de gérer les fonts découvrants sera introduite, suivie de quelques applications.
Considérons une variété M, définissable dans une structure o- minimale A, et munie d'un champ d'hyperplans H, intégrable et définissable dans A. Nous montrons qu'il existe un recouvrement fini de M par des ouverts définissables dans A sur chacuns desquels H induit un feuilletage en hypersurfaces séparantes.
Dans cet exposé, je présenterai une extension du lambda-calcul dans laquelle le filtrage s'effectue à l'aide d'une construction "case" (analyse par cas au sens du langage Pascal) se propageant à travers les fonctions comme une substitution linéaire de tête. Je montrerai en particulier que cette présentation du filtrage permet de récupérer toute l'expressivité du filtrage à la ML (avec des constructeurs non constants) et même plus. Ensuite, je présenterai la preuve du théorème de Church-Rosser, basée sur une technique inédite de "divide and conquer" dans laquelle on détermine de manière semi-automatique l'ensemble des paires de sous-systèmes qui commutent (en considérant toutes les combinaisons possibles des 9 règles de réduction primitives). Enfin, je montrerai que le calcul vérifie une propriété de séparation (non typée) dans l'esprit du théorème de Böhm.
ReactiveML est un langage de programmation dédié à la programmation de systèmes réactifs (e.g., simulation de systèmes dynamiques, interfaces graphiques, jeux video). Il est fondé sur le modèle "réactif synchrone" introduit par F. Boussinot. Ce modèle permet de combiner les principes de la programmation synchrone (composition parallèle synchrone de processus, communication par diffusion) et des mécanismes de création dynamique. Le langage est une extension conservative de Ocaml. Il ajoute des constructions supplémentaires pour décrire les comportements temporels des systèmes. Les programmes sont statiquement typés puis traduits en Ocaml. La première partie de cet exposé sera consacrée à la présentation du langage. La seconde partie présentera son implantation.
Dans cet exposé, nous proposons un modèle visqueux de type Saint-Venant avec une nouvelle force de Coriolis et nous en présentons diverses limites suivant les ordres de grandeur du nombre de Rossby et du nombre de Froude. Nous montrerons, plus précisemment, que l'extension au cas bidimensionnel des résultats unidimensionnels de [J.--F. Gerbeau, B. Perthame. Discrete Continuous Dynamical Systems, (2001)] en incluant la force de Coriolis nécessite d'inclure des termes nouveaux dépendant du cosinus de la latitude au sein des équations de Saint-Venant visqueux. On donnera ensuite les limites de type équations quasi- géostrophiques et équations des lacs correspondantes et nous finirons avec quelques propriétés mathématiques des modèles ainsi obtenus.
On montre que les ensembles extrémaux du gradient d'une fonction générique lisse sont lisses en dehors des points critiques de la fonction. Aux points critiques, les branches lisses des ensembles extrémaux sont tangents aux espaces propres du hessien. De plus, la fonction est de Morse sur son ensemble extrémal.
Les 8 et 9 Février 2007 auront lieu, à Chambéry, les rencontres du groupe LAC du GDR IM. Plus d'info sur la page de ces journées : www.lama.univ-savoie.fr/~david/gdr/journees.html
Sous-faisceaux dans les topologies de Grothendieck et si on a le temps topologies de Lawvere-Tierney
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.