Nous nous plaçons dans le contexte de la résolution à la Puiseux d’équations polynomiales en plusieurs variables. Notre objectif est de comprendre ce qui distingue une série de Puiseux multivariée algébrique (sur $K(x_1,....,x_r)$ le corps des fonctions rationnelles à r variables) d’une série de Puiseux formelle. Plus précisément, nous résolvons les problèmes suivants : - étant donnée une équation polynomiale $P(x_1,....,x_r,y)=0$, donner une formule pour les coefficients d’une série de Puiseux $y(x_1,....,x_r)$ solution en fonction des coefficients de l’équation ; - étant donnée une série de Puiseux algébrique, reconstruire à partir de ses coefficients un polynôme annulateur. Il s’agit d’une généralisation à plusieurs variables de notre travail sur les mêmes questions pour le cas monovarié. Travail en commun avec M. Hickel (Bordeaux).
La prévention d'une trop grande dispersion de pollens transgéniques est un sujet de grande importance dans l'agriculture moderne. Le mouvement du pollen transgénique se fait en grande partie par des insectes pollinisateurs, dont le plus important est l'abeille domestique, apis mellifera. Dans cet exposé, je vais présenter des modèles mathématiques pour le mouvement des abeilles, et montrer comment ces modèles peuvent nous aider à prédire la dispersion du pollen transgénique.
La sémantique d'un programme est souvent donnée d'une des deux façons suivantes: ou bien comme une fonction mathématique (la fonction qu'il calcule) ou bien par le biais de son execution. La première méthode tend à détruire toute information fine sur le programme (complexité par exemple), alors que la seconde impose un cadre de bas niveau, syntaxique, sans la structure et les propriétés mathématiques donnés par la première. Pour allier les avantages des deux méthodes, de nombreux sémanticiens s'intéressent à représenter les programmes comme des interactions (interactions qui se déroulent entre un programme et son contexte); ceci en permet une compréhension dynamique. Le lambda-calcul est un formalisme standard pour représenter les programmes fonctionnels. Le pi-calcul, lui, fournit un outil pour représenter leurs interactions. Milner a montré en 1990 comment interpréter le lambda-calcul dans le pi-calcul. Plus précisément, il a montré comment interpréter deux stratégies d'évaluations du lambda-calcul, l'appel par nom et l'appel par valeurs. Se pose alors le problème de Full Abstraction: pour quelle notion d'équivalence de programme ces interprétations sont-elles correctes et complètes ? Si le problème a été résolu rapidement pour l'appel par nom, l'appel par valeur pose davantage de problèmes techniques...
On étudie la stabilité d'une famille de solutions stationnaires de l'équation d'Euler dans R^3 qui décrivent des tourbillons à symétrie cylindrique : le champ de vitesse est dans le plan horizontal, et ne dépend que de la distance à l'axe vertical. Ces solutions ont été étudiées notamment par Kelvin et Rayleigh au 19ème siècle, mais les seuls résultats de stabilité obtenus jusqu'ici concernent des perturbations très particulières (bidimensionnelles ou axisymétriques). On donne une condition suffisante sur le profil de vitesse du tourbillon garantissant la stabilité spectrale vis-à-vis de perturbations arbitraires. Il s'agit d'un travail en collaborationa avec Didier Smets
Dans cet exposé, je présenterai un problème qui modélise le mouvement d'un solide dans un fluide visqueux incompressible. On s'intéresse ici à l'évolution d'un seul obstacle qui se rétrécit en une particule ponctuelle dans un fluide de R^2 ou R^3. On montrera la convergence des solutions du système fluide-solide vers une solution des équations de Navier-Stokes sans obstacle grâce aux estimations d'énergie.
L’inégalité de Smith-Thom borne la somme des nombres de Betti de la partie réelle d’une variété algébrique réelle par la somme des nombres de Betti de sa partie complexe. Dans cet exposé, nous expliquerons une preuve d’une conjecture d’Itenberg qui raffine cette borne pour une classe particulière d’hypersurfaces réelles projectives en termes de ses nombres de Hodge. Les hypersurfaces considérées proviennent de la construction du patchwork de Viro, qui est une méthode combinatoire puissante de construction d’hypersurfaces algébrique réelles. Pour démontrer la conjecture d’Itenberg, nous développons un analogue réel de l’homologie tropicale et, à l’aide d’une suite spectrale, nous la comparons à l’homologie tropicale définie par Itenberg, Katzarkov, Mikhalkin et Zharkov. L’homologie tropicale redonne les nombres de Hodge d’une variété projective complexe, et sa version réelle détermine les nombres de Betti de sa partie réelle. Comprendre plus en détail la suite spectrale apparaissant dans la preuve est une des clefs pour contrôler la topologie de l’hypersurface réelle provenant d’un patchwork.
Arnaud Duran vous parlait récemment, entre autres, du système de Green-Naghdi et des difficultés liées à sa résolution numérique. Une stratégie a été récemment proposée par Nicolas Favrie et Sergey Gavrilyuk : il s'agit de résoudre un système approché, qui a l'avantage d'être quasilinéaire hyperbolique (plus d'opérateur d'ordre élevé) et le défaut de mettre en jeu des variables supplémentaires et un paramètre de relaxation. Nous donnerons une justification rigoureuse de cette approche. Il s'agit d'un problème de limite singulière qui serait classique s'il ne dépendait de deux paramètres.
Guarded recursion has emerged as a natural paradigm for programming with infinite data structures in type theory and high-assurance functional languages. In the first part of this talk, I will present some intuitions behind guarded recursion, using programming examples. In a second part, I will discuss ongoing work on a typed lambda-calculus equipped with rich facilities for defining and manipulating guarded recursive types.
An Asynchronous Soundness Theorem for Concurrent Separation Logic. Concurrent separation logic (CSL) is a specification logic for concurrent imperative programs with shared memory and locks. We develop a concurrent and interactive account of the logic inspired by asynchronous game semantics. To every program C, we associate a pair of asynchronous transition systems ⟦C⟧S and ⟦C⟧L which describe the operational behavior of the Code when confronted to its Environment (or Frame) – both at the level of machine states (S) and of machine instructions and locks (L). We then establish that every derivation tree π of a judgment Γ⊢{P}C{Q} defines a winning and asynchronous strategy ⟦π⟧Sep with respect to both asynchronous semantics ⟦C⟧S and ⟦C⟧L. From this, we deduce an asynchronous soundness theorem for CSL, which states that the canonical map ℒ:⟦C⟧S→⟦C⟧L, from the stateful semantics ⟦C⟧S to the stateless semantics ⟦C⟧L satisfies a basic fibrational property. We advocate that this provides a clean and conceptual explanation for the usual soundness theorem of CSL, including the absence of data races. This is joint work with Paul-André Melliès. Organization of the talk: In a first part, I will give a high level view of our semantics and of the soundness theorem, essentially as it appeared in our previous paper. In a second part, I will talk in more details about our new semantics of CSL, which has a more algebraic flavor (work in progress).
Dans cet exposé nous nous intéressons au processus de rafle définie par un opérateur multivoque définissable dans une structure o-minimale. Nous établissons une inégalité de type KL adaptée au problème et nous l'utilisons pour montrer que les trajectoires bornées sont de longueur finie. Cette méthode permet d'obtenir le cas classique de la dynamique du gradient comme cas particulier, en onsidérant le processus de rafle correspondant aux sous-niveaux d'une fonction de classe C^1 o-minimale. Travail en collaboration avec D. Drusvyatskiy (Seattle).
Je parlerai des avancées récentes obtenues an collaboration avec Jérôme Poineau concernant la finitude dimensionnelle de la cohomologie de de Rham d'une équation différentielle sur une courbe p-adique. Cela est un problème profond et à la base de la théorie qui est resté ouvert pendant 50 ans.
Realizability and parametricity are two well-known approaches to the semantics of System F, the architectural language for polymorphism. Many well-known realizability semantics can be recast in a simple topological form as induced by closure operators over sets of lambda-terms. This allows to generalize some completeness results known in the literature to a wide class of semantics (including Krivine's saturated sets and several variants of Girard's reducibility candidates), and to relate realizability with parametricity and dinaturality, an approach to parametricity arising from the functorial semantics of polymorphism. Our main result is that for a general class of realizability semantics (those which satisfy a particular topological property) one can prove a parametricity theorem'' stating that closed realizers are parametric and adinaturality theorem'' stating that closed realizers of positive types are dinatural. We compare our results with Wadler's approach which sees realizability and parametricity as some sort of adjoint functors. Finally, we briefly discuss the case of Girard's original definition of reducibility candidates, whose ``not trivial and somehow mysterious'' [Riba 2007] structure does not fit yet within our approach.
Cette thèse porte sur des propriétés arithmétiques des fonctions méromorphes et transcendantes d'une variable. Nous définissons des mesures de transcendance pour les fonctions holomorphes ou méromorphes sur un domaine régulier du plan puis nous majorons ces mesures en fonction de la distribution des petites valeurs de la fonction étudiée. Grâce aux théories de Nevanlinna et d'Ahlfors, nous étudions la distribution des petites valeurs de certaines classes de fonctions méromorphes sur le disque ou le plan afin d'obtenir pour celles-ci des majorations explicites de leurs mesures de transcendance. L'application principale de ce travail est l'obtention de nouveaux lemmes de zéros polynomiaux pour de grandes familles de fonctions méromorphes et en particulier pour les fonctions elliptiques et les fonctions fuchsiennes. Ces lemmes de zéros polynomiaux conduisent à des bornes logarithmiques du nombre de points algébriques de degré et hauteur bornés contenus dans les graphes des fonctions étudiées.
La propagation des vagues dans les zones côtières implique des mécanismes complexes, représentant des enjeux de modélisation et numériques considérables. Si la plupart des processus non-linéaires sont généralement capturés par des modèles de type Boussinesq, ces équations conservent l’énergie et sont donc intrinsèquement inaptes à décrire les mécanismes dissipatifs, tels que ceux associés au déferlement des vagues par exemple. Pour gérer ce phénomène, nous introduisons un nouveau modèle dispersif fortement non-linéaire capable de prendre en compte les effets turbulents sous-jacents. L’approche est caractérisée par la présence d’une nouvelle variable basée sur la variation verticale de la vitesse, appelée enstrophie, modélisant l’énergie turbulente. Le modèle proposé partage une structure similaire aux équa- tions de Green-Naghdi et peut donc être intégré sur la base de tout modèle numérique existant pour ces équations. Dans le prolongement de travaux récents, nous considérons un discrétisation type Galerkin discontinue du système, basée sur un découplage entre les parties hyperboliques et non- hydrostatiques. Des validations numériques 1d et 2d impliquant la propa- gation de vagues déferlantes sur topographies non triviales sont proposées. En particulier, les comparaisons avec les données expérimentales confirment l’efficacité de la stratégie, mettant en évidence l’enstrophie comme un outil robuste et fiable pour la détection et la description des vagues déferlantes, même dans un cadre bidimensionnel.
J'expliquerai comment borner supérieurement la topologie d'un sous-complexe aléatoire dans un complexe simplicial, comment un empilement de simplexes disjoints permet d'améliorer ces bornes et comment un pavage permet d'obtenir de bons empilements. Il s'agit d'un travail en commun avec Nermin Salepci.
Sous l'égide de Maître Yoda: Guy Métivier; et avec les conférences de Jedi confirmés: Claude Zuily, Nicolas Burq, Raphael Danchin, Eric Dumas, David Lannes ainsi que la conférence de Christophe Lacave, représentant des Padaouanes travaillant en EDPs et méca flu au niveau national.
Durant ce séminaire nous présenterons le cadre général pour étudier des opérateurs agissant sur des systèmes périodiques discrets. Il s’agit des cristaux topologiques que nous perturberons ensuite de diverses manières. Les opérateurs de Schrödinger agissant sur ces structures seront alors étudiés du point de vue de la théorie spectrale et de la diffusion. A cette occasion, nous mettrons également en évidence des outils issus de l'analyse fonctionnelle qui sont certainement peu utilisés en géométrie (théorie de Mourre, construction d'un opérateur conjugué).
Que peut-on dire de deux variétés algébriques ayant la même classe dans l'anneau de Grothendieck des variétés? Un espoir (déçu) était de montrer qu'elles étaient isomorphes par morceaux. On montrera que c'est le cas dans le cadre des ensembles symétriques par arcs en géométrie algébrique réelle.