On propose une extension naturelle du λ-calcul autorisant la formation de combinaisons linéaires de termes. Ceci reflète dans la syntaxe la sémantique quantitative du λ-calcul simplement typé dans les espaces de finitude, où les types sont interprétés par des espaces vectoriels particuliers, et les λ-termes par des fonctions entre ces espaces.
On étudie les effets de la présence de coefficients scalaires sur la réduction: après avoir étendu la β-réduction en une relation contextuelle et confluente, on s'intéresse à la cohérence du calcul et à des propriétés de normalisation dans un cadre typé.
On établit enfin une correspondance entre ce λ-calcul algébrique et le λ-calcul linéaire-algébrique d'Arrighi et Dowek en montrant qu'ils correspondent à deux stratégies de réduction (par nom et par valeur) d'une syntaxe commune.
Le contrôle quantique, c'est-à-dire le contrôle de processus physico-chimiques par laser, a connu de nombreux développements - tant théoriques qu'expérimentaux - au cours de la dernière décennie. Parallèlement à l'expérimentation, la simulation numérique a contribué de manière significative à la conception de champs lasers efficaces. Nous présentons ici une classe d'algorithmes d'optimisation associée aux fonctionnelles de coût rencontrées en chimie quantique, les schémas monotones. Basés sur des résolutions itératives de l'équation de Schrödinger, ces algorithmes ont la particularité de faire croître de manière monotone les fonctionnelles considérées. D'un point de vue numérique, une discrétisation en temps adaptée a été conçue de manière à préserver cette propriété au niveau du schéma de calcul. La convergence de la suite des champs de contrôle Laser ainsi obtenue est prouvée en utilisant l'inégalité de Lojasiewicz. Enfin, nous présentons une méthode de parallélisation en temps de ces schémas qui permet, lors de premiers tests numériques, de diminuer d'un ordre de grandeur le coût computationnel de l'optimisation, sans pour autant modifier le champs laser limite.
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.