Séminaires de l'année

Aujourd'hui, la compréhension et le contrôle de phénomènes complexes issus de la dynamique des fluides nécessitent le développement et l'utilisation d'outils de simulation numérique spécifiquement conçus et adaptés au contexte applicatif. Ceci permet de garantir la fiabilité et la pertinence des résultats obtenus, et constitue donc un enjeu majeur pour une multitude d'applications, notamment industrielles ou environnementales. Dans cet exposé, nous présentons la mise au point d'un schéma numérique hybride volumes finis / éléments finis basé sur un splitting en temps, pour la résolution des équations de Navier-Stokes incompressibles à densité variable. On montre en particulier que ce schéma permet de simuler des phénomènes instables de type Rayleigh-Taylor, en alliant précision et robustesse. Puis nous simulons l'écoulement d'un fluide visqueux incompressible en régime transitoire au dessus d'une marche descendante par une méthode vortex pour l'étude des zones rotationnelles. Une stratégie de contrôle actif est alors développée, permettant d'affiner la compréhension du processus de déclenchement tourbillonnaire et de le contrôler.

We analyze the moment of inertia $\MI(S)$, relative to the center of gravity, of finite plane lattice sets $S$. We classify these sets according to their roundness: a set $S$ is rounder than a set $T$ if $\MI(S) < \MI(T)$. We show that roundest sets of a given size are strongly convex in the discrete sense. Moreover, we introduce the notion of quasi-discs and show that roundest sets are quasi-discs. We use weakly unimodal partitions and an inequality for the radius to make a table of roundest discrete sets up to size $40$. Surprisingly, it turns out that the radius of the smallest disc containing a roundest discrete set $S$ is not necessarily the radius of $S$ as a quasi-disc.

Je présenterai dans cet exposé les résultats obtenus récemment en collaboration avec Ying Hu sur les Équations Différentielles Stochastiques Rétrogrades quadratiques à coefficients non bornés. Si les résultats d'existence pour ce type d'équations sont satisfaisants, nous verrons que l'étude de l'unicité s'avère plus délicate et nécessite des hypothèses plus contraignantes. Il est néanmoins possible d'obtenir des résultats suffisamment précis pour obtenir, dans ce contexte, la formule de Feynman-Kac qui donne une représentation probabiliste de la solution d'une EDP non-linéaire quadratique dans le gradient de la solution. Je préciserai également les problèmes qui demeurent sans réponse pour ce type d'équations du point de vue de l'unicité comme du point de vue de l'approximation.

Cet exposé a pour but de nous révéler que la géométrie de Hilbert d'un domaine polygonal convexe est Lipschitz équivalente au plan euclidien.

Deuxième édition du séminaire Choco.
Le programme prévu est le suivant:
10h - 12h Damiano Mazza (PPS, Paris), Objets d'interaction et réseaux différentiels
14h - 15h30 Michele Pagani (PPS, Paris), Between interaction and semantics: visible acyclic nets
16h - 17h30 Lionel Vaux (IML, Marseille), Produit de convolution et composition parallèle

Je m'intéresse au modèle d'Euler-Poisson pour modéliser un plasma contenant à la fois des régions quasi-neutres et non quasi-neutres. Les discrétisations explicites classiques de ce système souffrent de contraintes numériques très sévères. Elles sont reliées à deux quantités bien connues en physique des plasmas qui sont la longueur de Debye et la période plasma. Ces discrétisations doivent résoudre ces deux échelles afin d'etre stables et consistantes. Or, dans les régions quasi-neutres la longueur de Debye et la période plasma sont très petites. Les couts calculs sont tels qu'il n'est pas possible de réaliser des simulations réalistes en dimensions deux ou trois. Je présenterai un schéma préservant l'asymptotique quasi-neutre, c'est à dire ne nécessitant pas la résolution des petites échelles pour assurer la stabilité et permettant de récupérer une discrétisation du régime quasi-neutre dans la limite quasi-neutre. De plus, une propriété importante de ce schéma est que, pour un pas de temps et un pas d'espace donnés, son cout calcul est le meme que les schémas explicites précédemment cités. Enfin, je terminerai mon exposé, par la description d'un problème de couche limite apparaissant dans la limite quasi-neutre lorsque les conditions aux limites ne sont pas bien préparées au régime quasi-neutre. Cette couche limite doit etre résolue afin d'assurer la stabilité des discrétisations. Je montrerai qu'en introduisant un développement formel de cette couche limite, on peut déterminer des données aux limites bien préparées permettant de s'affranchir de la résolution de la couche limite.

Dans cet exposé, on considère la résolution numérique de problèmes de contact unilatéral de type Signorini en élasticité linéarisée par des méthodes des éléments finis. En discutant de modélisations de problèmes de contact complexes issues d'applications non académiques, on montre la nécessité d'introduire de nouveaux outils de discrétisation dans le domaine de la mécanique de contact. A cet effet, on propose une méthode de domaine fictif comme nouveau cadre de résolution de tels problèmes dans des domaines géométriques complexes et/ou en mouvement. Cette nouvelle méthode de discrétisation permet, en plus de la gestion de zones de contacts qui varient, d'utiliser des stratégies adaptatives efficaces (optimales) de résolution qui sont nécessaires pour ces problèmes souvent complexes et aux coûts de résolution élevés. On présente des résultats de simulations numériques en accord avec les estimations théoriques et qui montrent l'intérêt de cette approche (méthode de domaine ficitf et adaptativité) pour résoudre ces problèmes difficiles.

(En collaboration avec André et Michel Hirschowitz.)
La sémantique des jeux a fait ses preuves comme source de modèles pleinement abstraits pour langages de programmation ou théories de la démonstration. De tels modèles apparaissent comme catégories de jeux et stratégies, mais on en compte de nombreuses variantes, qu'on ne sait pas bien relier entre elles. D'où la question: qu'est-ce qu'une catégorie de jeux et stratégies?
On donne une définition catégorique générale de jeu, en décrivant la catégorie de stratégies associée. On définit ensuite une construction catégorique générant un jeu à partir de données plus élémentaires. On montre comment les jeux de Hyland et Ong avec switching entrent dans ce cadre.

Des problèmes hyperboliques à coefficients discontinus apparaissent suite à la modélisation de certains phénomènes physiques. Ces problèmes, pris tels quels, n'ont en général pas de sens classique, c'est pourquoi une autre approche doit être proposée. Il s'agit là d'une thématique de recherche sur laquelle ont notamment travaillé Bouchut et James, LeFloch, Bachmann et Vovelle, Poupaud et Rascle, ... Mon exposé portera sur divers problèmes linéaires hyperboliques du premier ordre, discontinus au travers d'une hypersurface non-caractéristique fixée. La motivation est ici l'étude de la propagation d'ondes linéaires en présence d'une interface fixée, joignant par exemple deux fluides compressibles associés à des lois d'état différentes. L'approche choisie est une approche à viscosité évanescente. Nous montrons, dans différents cadres, que cette approche permet de sélectionner une unique solution à petite viscosité au problème. On verra en particulier que la nature de l'interface joue un rôle prépondérant.

We define (with machine-checked proofs in Coq) a modular operational semantics for Concurrent C minor---a language with shared memory, spawnable threads, and first-class locks. By modular we mean that one can reason about sequential control and data-flow knowing almost nothing about concurrency, and one can reason about concurrency knowing almost nothing about sequential control and data-flow constructs. We present a Concurrent Separation Logic with first-class locks and threads, and prove its soundness with respect to the operational semantics. Using our modularity principle, we proved the sequential CSL rules (those that are inherited from sequential Separation Logic) simply by adapting Appel & Blazy's machine-checked sequential-separation-logic soundness proofs with minimal changes. Our Concurrent C minor operational semantics is designed to connect to Leroy's optimizing (sequential) C minor compiler; we propose our modular semantics as a way to adapt Leroy's compiler-correctness proofs to the concurrent setting. Thus we will obtain end-to-end proofs: the properties you prove in Concurrent Separation Logic will be true of the program that actually executes on the machine. (Joint work with Aquinas Hobor and Andrew Appel (Princeton University)).

TBA

Nous présentons une classe de modèles du lambda-calcul et de la logique du second ordre. Les modèles sont basés sur des treillis et interprètent la réduction, ainsi que la relation de réalisabilité, à l'aide de la relation d'ordre. Nous tenterons de dégager les liens avec les algèbres de Heyting et les modèles à base de cpo du lambda-calcul.

TBA

Le système de Keller-Segel décrit simplement une instabilité due à la chemotaxie, lorsque des cellules s'attirent mutuellement via un signal chimique (des exemples issus de la modélisation illustrent cette instabilité). Nous étudions des généralisations du modèle de Keller-Segel, incluant notamment une diffusion nonlinéaire des cellules, ou bien une loi de diffusion chimique à noyau de Green logarithmique. Puis nous proposons une formulation de type Wasserstein qui permet d'analyser efficament le cas de la dimension 1 d'espace. Cette nouvelle approche permet de mieux appréhender la géométrie du modèle de Keller-Segel. Ce travail est le fruit de collaborations avec Adrien Blanchet, José Carrillo, et Hossein Khonsari.

La question de l'existence de certaines surfaces quartique de P^3(R) a été posée par Hilbert dans la première partie de son 16° problème. En 1975, Kharlamov a montré l'existence de ces surfaces quartiques de P^3(R) par une méthode non constructive. En 1979, Viro a montré comment, en partant de courbes sur l'hyperboloïde, on pouvait prouver directement l'existence des surfaces quartiques P^3(R) considérées. Mais Viro ne détaille pas la construction de toutes les courbes utilisées. Dans cet exposé, on construira explicitement les courbes réelles de genre 9 avec 10 composantes connexes nécessaires et on appliquera ce résultat aux surfaces quartiques.

We argue in favor of the following thesis: there is an intric link between the computation we can unwing from classical proofs and parallel computations. We introduce a model for computations extracted from classical proofs based on parallel computations and on the concept of learning in the limit. The aim of our research is designing parallel extensions of the existing continuation languages.