Le traitement catégorique de la théorie des probabilités formulé par Giry et Lawvere, basé sur la monade de probabilité G, permet de manipuler de façon élégante des probabilités d'ordre supérieur. Dans ce cadre, je présenterai une reconstruction du processus de Dirichlet, un objet largement utilisé en inférence bayésienne. Ce processus prend la forme d'une famille de mesures dans GG(X) indexée par M(X), où X est un espace Polonais et M(X) est l'espace des mesures finies non-zéro sur X. Sa construction repose sur deux outils dont l’intérêt dépasse le simple cas de la construction de Dirichlet. Le premier de ces outils est une version fonctorielle du théorème d'extension de Bochner adapté au cadre Polonais, qui permet d'étendre une famille projective de probabilités en une probabilité limite. Le second outil est une méthode de ``décomposition'' qui associe à tout espace Polonais zéro-dimensionnel une famille projective d'espaces finis, dont la limite projective est une compactification de l'espace originel. La combinaison de ces deux outils avec des propriétés bien connues de Dirichlet sur les espaces finis nous permet de reconstruire Dirichlet comme une transformation naturelle de M vers GG. Cette construction améliore les précédentes en ce qu'elle prouve la continuité de Dirichlet en ses paramètres.
PML est un langage de programmation en appel par valeurs similaire à ML, avec une syntaxe à la Curry (c'est à dire, pas de types dans les termes) et basé sur une logique d'ordre supérieur classique. Les termes apparaissent dans les types via un prédicat d'appartenance t ∈ A et un opérateur de restriction A | t ≡ u. La sémantique de ces deux constructeurs de types utilise une relation d'équivalence (observationnelle) sur les programmes (non typés). L'opérateur de restriction est utile pour l'écriture de spécifications tandis que l'appartenance permet d'encoder les types dépendants. La présence de l'équivalence nous permet également de relâcher la « value restriction » pour obtenir un type produit dépendant compatible avec la logique classique (ce qui n'avait pas été fait avant).
La théorie des jeux à champ moyen a été initée par Lasry et Lions il y a une dizaine d'années. Le but est de décrire le comportement asymptotique d'équilibres de Nash sur une grande population de joueurs en interaction champ moyen. Dans ce cadre, très peu de critères sont connus pour garantir l'unicité des équilibres asymptotiques. Inspirés par la théorie des EDO et EDS, nous posons ici la question du rétablissement de l'unicité par randomisation des solutions.
We call a closed basic semialgebraic subset X of R^n homogeneous if it is defined by a finite system of strict inequalities with homogeneous polynomials. We prove an effective version of the Putinar and Vasilescu Positivstellensatz for positive homogeneous polynomials on homogeneous semialgebraic sets.
L'espace des arcs centrés en un point donné d'une variété a une structure de cône, qui induit une structure d'algèbre graduée sur l'algèbre de l'espace des arcs. La série de Hilbert-Poincaré associée à cette algèbre est un invariant des singularités. Je vais introduire cet invariant, parler de son calcul pour certaines singularités et d'une relation entre cette série et une fameuse identité de la théorie des partitions, qui est due à Rogers et à Ramanujan. C'est un travail en commun avec Clemens Bruschek et Jan Schepers.
Le ``size-change principle'' (SCP) est un algorithme simple donnant un test partiel de terminaison qui s'adapte très bien aux langages fonctionnels où les fonctions sont définies de manière récursive par pattern-matching. En présence de constructeurs paresseux, le SCP donne également un test (partiel) de productivité : c'est sur ce principe que les tests (terminaison + productivité) de PML et Agda reposent. Malheureusement, en présence de type coinductifs, certaines définitions récursives bien typées terminent (i.e. sont productives) mais sont incorrectes et rendent Agda/PML inconsistants. En utilisant les travaux de L. Santocanale sur les preuves circulaires et les jeux de parité, je montrerais comment utiliser le SCP pour implanter un test partiel de totalité des définitions récursives qui généralise le test de terminaison/productivité, et garantie qu'une définition est correcte vis à vis de son type.
Le travail à présenter est une contribution à la spécification et la vérification des Systèmes à Base de Composants (SBC) modélisés avec le langage SysML. Les SBC sont largement utilisés dans le domaine industriel et ils sont construits en assemblant différents composants réutilisables, permettant ainsi le développement de systèmes complexes en réduisant leur coût de développement. Malgré le succès de l’utilisation des SBC, leur conception est une étape de plus en plus complexe qui nécessite la mise en œuvre d’approches plus rigoureuses. Dans ce contexte, nous allons traiter principalement deux problématiques: La première est liée à la difficulté de déterminer quoi construire et comment le construire, en considérant seulement les exigences du système et des composants réutilisables, donc la question qui en découle est la suivante : comment spécifier une architecture SBC qui satisfait toutes les exigences du système ? Nous proposons une approche de vérification formelle incrémentale basée sur des modèles SysML et des automates d’interface pour guider, par les exigences, le concepteur SBC afin de définir une architecture de système cohérente, qui satisfait toutes les exigences SysML proposées. Dans cette approche nous exploitons le Model Checker SPIN et la LTL pour spécifier et vérifier les exigences. La deuxième problématique traitée concerne le développement par raffinement d’un SBC modélisé uniquement par ses interfaces SysML. Notre contribution permet au concepteur des SBC de garantir formellement qu’une composition d’un ensemble de composants élémentaires et réutilisables raffine une spécification abstraite d’un SBC. Dans cette contribution, nous exploitons les outils : Ptolemy pour la vérification de la compatibilité des composants assemblés, et l’outil MIO pour la vérification du raffinement.
In this talk we will focus on two-fluid formulations where the fluids are assumed to be compressible and viscosity effects are included in the momentum equations. In the introduction we try to motivate for the study of this model: why can such models be a useful tool for engineers. Then we will narrow the scope and describe a two-fluid model for cell migration. This model can be understood as a generalization of more classical Keller-Segel type of models for cell migration due to random motion and chemotaxis. The model takes the form of a (weakly) compressible two-fluid model with non-conservative pressure terms and interaction terms that play a key role in the momentum equations. The link to Keller-Segel type of models is established by imposing simplifying assumptions and making a specific choice of the interaction term. Existence of global regular solutions for the proposed model for cell migration is then obtained for sufficiently small and regular initial data. The central ingredient in the proof is a basic energy estimate which is combined with certain higher order estimates of cell mass, water mass, and mass of the chemical agent. We also include some examples of numerical solutions of the proposed model that demonstrate pattern formation properties characteristic for Keller-Segel type of models. Sensitivity to different parameters is explored. Finally, we also show some numerical results for a 2D version of a similar model.
It is long known that any expansion, M, of the field of real numbers that defines N (the set of all natural numbers) also defines every real Borel set, hence also every real projective set (in the sense of descriptive set theory). Thus, one can easily ask questions about the definable sets of M that turn out to be independent of ZFC (e.g., whether every definable set is Lebesgue measurable). This leads naturally to wondering what can be said about its definable sets if M does not define N. Philipp Hieronymi (Urbana-Champaign) and I have recently obtained a result that can be stated loosely as: M avoids defining N if and only if all metric dimensions commonly encountered in geometric measure theory, fractal geometry and analysis on metric spaces coincide with topological dimension on all images of closed definable sets under definable continuous maps. I will make this statement precise (assuming essentially no knowledge of model theory or dimension theory), explain its significance, and give some easy (yet striking) corollaries and applications.
I will report on some recent progress on optimization problems involving the first Dirichlet eigenvalue and the torsional rigidity. This is joint work with G. Buttazzo, B. Velichkov and with C. Trombetti, C. Nitsch, V. Ferone.
The M2Disco (Multiresolution, Discrete and Combinatorial Models) research team aims at proposing new combinatorial, discrete and multiresolution models to analyse and manage various types of data such as images, 3D volumes and 3D meshes, represented as Digital Sur- faces (ie subset of Zn). One of their project called PALSE foam requires the computation of the shortest path between two points on a manifold. We are proposing the study of two algorithm for computing such a dis- tance, but also providing metric embedding inside a Discrete Exterior Calculus structure (DEC). We performs various tests regarding the two algorithms, but also con rm through experience DEC's operators con- vergence using suitable metric. This work is the base of both a research project named CoMeDiC (Convergent Metrics for Digital Calculus) and Ph.D. project.
L'équation Landau est une caricature ``diffusive'' de l'équation de Boltzmann, décrivant la densité de particules interagissant lors de chocs. Nous allons nous intéresser ici à l'approximation particulaire de l'équation de Landau dans le cas Maxwellien ou sphère dure et montrerons comment établir la propriété de propagation du chaos soit le fait que la loi d'une particule approche la solution de l'équation de Landau et que deux particules typiques sont presque indépendantes. (en collaboration avec F. Bolley (P6) et N. Fournier (P6))