Nous allons discuter le problème de comptage des cycles limites pour l'équation de Liénard classique x' = y - P(x) , y' = -x , où P(x) est un polynôme en x. Une compactification convenable de l'espace de tous les systèmes de Liénard nous amène à considérer l'équation du titre.
Je présenterai d'abord un développement formel à propos des fondements de la géométrie. Celui-ci consiste en la formalisation des huit premiers chapitres du livre de Schwabäuser, Szmielew et Tarski: Metamathematische Methoden in der Geometrie. Ensuite, je décrirai l'implantation en Coq d'une procédure de décision pour la géométrie affine plane: la méthode des aires de Chou, Gao et Zhang. Dans la troisième partie, nous nous intéresserons à la conception d'une interface graphique pour la preuve formelle en géométrie : Geoproof (http://home.gna.org/geoproof/). GeoProof combine un logiciel de géométrie dynamique avec l'assistant de preuve Coq. Enfin, je presenterai un système formel diagrammatique qui permet de formaliser des raisonnements dans le domaine de la réécriture abstraite. Il est par exemple possible de formaliser dans ce système la preuve diagrammatique du lemme de Newman. La correction et la complétude du système sont prouvées vis-à-vis d'une classe de formules appelée logique cohérente.
Nous savons maintenant qu'il existe dans la nature des modèles de la logique classique qui sont aux catégories ce que les algèbres de Boole sont aux ensembles ordonnés. Durant des années on a cru que de tels êtres ne pouvaient exister, étant donné le célèbre 171 paradoxe de Joyal 187 : une catégorie cartésienne fermée ne peut être équipée d'une négation symétrique. Les premiers exemples étaient des catégories de réseaux de démonstrations. Nous avons ensuite construit des sémantiques dénotationnelles pour la logique classique qui ressemblent beaucoup aux espaces cohérents. L'exposé se concentrera sur les propriétés essentielles que tous ces modèles possèdent, en d'autres termes sur les raisons pour quoi ça marche. Ces modèles nous mènent à nous poser des questions sur l'universalité de l'isomorphisme de Curry-Howard : il existe des façons de dénoter des preuves en logique classique pour lesquelles le processus de normalisation ne correspond pas au calcul en programmation fonctionnelle. Les connaissances en théorie des catégories que nous supposons de la part de l'autitoire sont absolument minimales : les définitions de catégorie, foncteur et transformation naturelle.
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