Séminaires de l'année

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.

Dans les années quatre-vingt-dix, on a remarqué ce que l'isomorphisme de Curry-Howard peut être étendu à la logique classique. De nombreux calculs ont été développés pour constituer la base de cette extension. On étudie dans cette thèse quelques uns de ces calculs.
On étudie tout d’abord le lambda-mu-calcul simplement typé de Parigot. Parigot a prouvé par des méthodes sémantiques que son calcul est fortement normalisable. Ensuite, David et Nour ont donné une preuve arithmétique de la normalisation forte de ce calcul avec la règle mu' (règle duale de mu). Cependant, si l'on ajoute au lambda-mu-mu'-calcul la règle de simplification rho, la normalisation forte est perdue. On monte que le mu-mu'-rho-calcul non-typé est faiblement normalisable et que le lambda-mu-mu'-rho-calcul typé est aussi faiblement normalisable. De plus, on examine les effets d'ajouter quelques autres règles de simplification. On établit ensuite une borne de la longueur des séquences de réduction en lambda-mu-rho-theta-calcul simplement typé. Ce résultat est une extension de celui de Xi pour le lambda-calcul simplement typé. Enfin, on présente une preuve arithmétique de la normalisation forte du lambda-calcul symétrique de Berardi et Barbanera.

Des familles inductives de types de données servent bien à représenter le lambda-calcul: le paramètre de la famille décrit l'ensemble de noms de variables libres admises, et le changement du paramètre au cours de la récurrence reflète la génération de noms pour les variables liées. Cette représentation satisfait les propriétés de base de la substitution, dictées par la théorie des catégories. C'est bien connu.
On veut aller plus loin: On encapsule des sous-expressions de lambda-termes comme si elles n'étaient que des noms de variables libres. Ceci donne le lambda-calcul avec aplatissement explicite (une forme de substitution explicite). Sa représentation par une famille inductive requièrt des principes d'induction qui ne sont offertes par aucun assistant de preuves, or elles pouvaient être encodées dans Coq. Là, déjà la notion d'une occurrence libre d'une variable est un défi pour la conception mathématique.
Heureusement, la vérification entière se fait dans Coq, le plus grand problème étant un affaiblissement de la règle que la substitution qui remplace chaque variable par le terme qui consiste de cette variable n'a aucun effet. En plus, toute notre théorie axiomatique est justifiée dans le calcul des constructions inductives avec insignifiance des preuves.

Ce texte de synthèse a pour but de présenter l'évolution de mes recherches postèrieures à ma thèse. Ce travail s'articule autour de plusieurs axes de recherche dans le cadre des équations aux dérivées partielles non linéaires et en particulier des lois de conservation. Il s'inscrit dans l'étude des problèmes hyperboliques, des problèmes mixtes et des équations cinétiques. Les domaines d'application sont la mécanique des fluides ou du solide, la propagation de composants chimiques, l'électromagnétisme, l'optique. Mon activité concerne d'abord la modélisation de phénomènes physiques ou chimiques sous forme d'équations aux dérivées partielles non linéaires telles que les équations de Bloch, Korteweg, Navier-Stokes, Saint-Venant, puis vient l'étude mathématique de ces équations à travers les problèmes d'existence, d'unicité, de régularité avec éventuellement la mise au point de méthodes numériques de résolution. Ce document est divisé en une introduction générale et trois chapitres qui concernent respectivement les systèmes hyperboliques avec conditions aux limites et la chromatographie, les problèmes d'analyse asymptotique et enfin les méthodes cinétiques. Dans chaque partie, un historique et une présentation des différents résultats mathématiques sont faits et quelques problèmes ouverts sont donnés.

Dans cet exposé, on présentera des bornes sur la topologie d'un hypersurface fewnomiale qui améliorent grandement celles précédemment connues. Ces nouvelles bornes utilisent celles obtenues récémment par l'orateur et Frank Sottile sur le nombre de solutions positives de systèmes fewnomiaux. On montrera aussi, si le temps le permet, comment on peut modifier légèrement la preuve de de ces dernières bornes de manière à en obtenir d'autres sur le nombre de solutions réelles, qui soient également asymptotiquement optimales.

We introduce a new curvature estimator based on global optimisation. This method called Global Min-Curvature exploits the geometric properties of digital contours by using local bounds on tangent directions defined by the maximal digital straight segments. The estimator is adapted to noisy contours by replacing maximal segments with maximal blurred digital straight segments. Experimentations on perfect and damaged digital contours are performed and in both cases, comparisons with other existing methods are presented.

Dans une première partie, nous présentons des équations de Saint-Venant. Sur le modèle proprement dit, nous remarquons tout d'abord que, suivant le lien entre la viscosité et le rapport d'aspect, il est indispensable de conserver l'expression complète de la force de Coriolis : nous obtenons ainsi un nouveau modèle, avec un ``effet cosinus''. Nous montrons alors que les preuves d'existence de solutions faibles peuvent être adaptées à ce nouveau système. Des simulations numériques de certaines ondes soulignent l'importance de ce terme. Nous étudions ensuite l'influence des conditions limites (surface, fond) et du tenseur des contraintes sur des modèles de type Saint-Venant. Nous présentons également des modèles obtenus en utilisant des échelles multiples en espace et en temps. Enfin, nous analysons théoriquement et numériquement un nouveau modèle de sédimentation puis nous donnons certains résultats pour les fluides visco-plastiques. Dans une deuxième partie, nous nous intéressons aux équations limites que sont les équations quasi-géostrophiques (QG) et les équations des lacs. L'étude numérique des équations QG 2d met en évidence le rôle de l'effet cosinus de la force de Coriolis. En fonction de la topographie considérée, nous montrons que celui-ci peut être non négligeable. Toujours sur les équations QG, nous donnons un schéma, basé sur des développements asymptotiques, qui permet de bien capter la couche limite mais aussi d'ajouter le terme de topographie à la solution obtenue avec fond plat, sans tout recalculer. Enfin, nous expliquons l'obtention des équations des lacs avec effet cosinus, et nous prouvons que les propriétés d'existence de solutions restent valables.