Dependant Linear PCF (dlPCF) was introduced by Dal Lago and Gaboardi as a type system characterising the complexity of PCF programs. It is parametrised by a an equational program, which is used to express some complexity annotations for types. This enables a modular complexity analysis, and the main strength of the system is to be relatively complete: any terminating PCF program is typable in dlPCF (and its complexity is thus determined) assuming that the equational program is expressive enough. We have designed a type inference algorithm for this system: given a PCF program, it computes its type in dlPCF (and thus a complexity bound for the program) together with a set of proof obligations that ensures the correctness of the type, following the same scenario as the computation of weakest preconditions in Hoare logic. Checking formally the proof obligations generated by the type checker then amounts to a formal proof that the complexity bound is correct. In this talk I will explain how the type system dlPCF can be turned into a tool for formal certification of the complexity of functional programs.
Given any complex Laurent polynomial f we give an efficiently constructible polyhedral approximation of the amoeba of f, i.e., the image of the complex zero set of f under the log absolute value map. We call our polyhedral approximation the Archimedean tropical variety. Our main result is an explicit upper bound (as a function of the sparsity of f) for the Hausdorff distance between these two sets. We thus obtain an Archimedean analogue of Kapranov's Non-Archimedean Amoeba Theorem, and a higher-dimensional extension of earlier estimates of Mikhalkin and Ostrowski. As applications, we obtain efficient approximations for the possible norms of complex roots of polynomial systems, and an alternative, arguably more geometric proof of a formula of Khovanski relating lattice points in polygons and curve genus.
Dans cet exposé, je m'intéresserai à un système couplant les équations de Navier Stokes avec les lois de Newton qu'il est classique de considérer pour calculer le déplacement de solides dans un fluide visqueux incompressible. Je rappellerai tout d'abord les résultats connus sur la théorie de Cauchy. Je développerai ensuite un résultat obtenu en collaboration avec S. Ervedoza et C. Lacave sur la décroissance en temps des solutions dans le cas bidimensionnel où un disque homogène se déplaçe dans une cavité infinie.``
À venir
La géométrie spectrale est une branche des mathématiques relativement jeune, et qui se développe très rapidement. Son âge d'or s'est amorcé, entre autre, sous l'influence de Marc Kac qui, en 1966, formula la célèbre question: ``Can one hear the shape of a drum?''. La géométrie spectrale étudie les liens entre la géométrie d'un espace et les valeurs propres d'un opérateur (Laplacien, Dirac, de Schrödinger, etc) agissant sur les fonctions de cet espace. Dans cet exposé, je me concentrerai sur le spectre de l'opérateur de Dirichlet-Neumann. Cet opérateur agit sur les fonctions du bord d'une variété Riemannienne. Son spectre est connu sous le nom de spectre de Steklov de la variété. Je m'attarderai principalement aux aspects isopérimétriques. Les résultats que je présenterai ont été obtenus en collaboration avec Iosif Polterovich, ainsi qu'avec Bruno Colbois et Ahmad El Soufi. Plusieurs de ces résultats semblent indiquer que le spectre de l'opérateur Dirichlet-Neumann est lié à la géométrie sous-jacente de manière similaire au spectre de l'opérateur de Laplace-Beltrami, mais nous verrons qu'il existe des exemples où ces liens sont tout à fait différents, et peut-être même surprenants.
En géométrie algébrique complexe, les relations entre les fibres de Milnor et les espaces d'arcs d'une fonction polynomiale sont riches, illustrées notamment par les travaux sur les fonctions zêtas motiviques de Denef & Loeser, Nicaise & Sebag et plus récemment Hrushovski & Loeser. Dans le cadre réel, l'absence de monodromie complique la compréhension et rend mystérieuses ces relations. Dans l'exposé, on considère un objet (faiblement o-minimal) composé de séries de Puiseux réelles qui pourrait créer un pont entre ces aspects topologiques et algébriques. On montre en particulier que l'objet en question rend compte de l'homologie de la fibre de Milnor réelle.
On examinera des propriétés d'algèbre pour des espaces de Sobolev fractionnaires sur des groupes de Lie ou des variétés riemanniennes. Deux approches seront proposées. Ces propriétés seront appliquées à l'étude de certaines EDP semilinéaires. Il s'agit de travaux avec N. Badr (Lyon I) et F. Bernicot (Nantes).
J'expliquerai que dans R^n, le nombre moyen de composantes connexes d'une hypersurface algébrique réelle aléatoire de degr'e d est plus grand que exp(-70 exp(n)) sqrt d^n, pour d assez grand. La démonstration repose sur la résolution du dbar avec estimées L^2 de Hörmander, et c'est un travail en commun avec Jean-Yves Welschinger.
La logique, et plus particulièrement la théorie de la démonstration — domaine qui a pour objet d'étude les preuves mathématiques, a récemment donné lieu à de nombreux développements concernant l'informatique théorique. Ces développements se fondent sur une correspondance, dite de Curry-Howard, entre les preuves mathématiques et les programmes informatiques. L'intérêt de cette correspondance provient du fait que celle-ci soit dynamique: l'exécution des programmes correspond à une procédure sur les preuves, dite d'élimination des coupures. Suite à une étude poussée de la formalisation des preuves, Jean-Yves Girard a initié le programme de géométrie de l'interaction. Ce programme, dans une première approximation, a pour objectif l'obtention d'une représentation des preuves rendant compte de la dynamique de l'élimination des coupures. Via la correspondance entre preuves et programmes, cela correspond donc à obtenir une sémantique des programmes rendant compte de la dynamique de leur exécution. Cependant, le programme de géométrie de l'interaction est plus ambitieux: au-delà de la simple interprétation des preuves, il s'agit d'une complète reconstruction de la logique autour de la dynamique d'élimination des coupures. On reconstruit donc la logique des programmes eux-mêmes, dans un cadre où la notion de formule rend compte du comportement des algorithmes. Depuis l'introduction de ce programme, Jean-Yves Girard a proposé plusieurs constructions afin de le réaliser dans lesquelles les preuves sont représentées par des opérateurs dans une algèbre de von Neumann. Ces constructions étant fondées sur la notion d'exécution des programmes, le programme de géométrie de l'interaction est particulièrement pertinent pour l'étude de la complexité algorithmique. En particulier, ce programme a déjà démontré qu'il permettait de formaliser à l'aide d'outils mathématiques des classes de complexité en temps et en espace.
A series of recent papers introduces a coalgebraic semantics for logic programming, where the behavior of a goal is represented by a parallel model of computation called coinductive tree. This semantics fails to be compositional, in the sense that the coalgebra formalizing such behavior does not commute with the substitutions that may apply to a goal. We suggest that this is an instance of a more general phenomenon, occurring in the setting of interactive systems (in particular, nominal process calculi), when one tries to model their semantics with coalgebrae on presheaves. In those cases, compositionality can be obtained through saturation. We apply the same approach to logic programming: the resulting semantics is compositional and enjoys an elegant formulation in terms of coalgebrae on presheaves and their right Kan extensions.
Le théorème d'Abhyankar-Jung affirme que les racines d'un polynôme à coefficients des séries formelles sur un corps de caractéristique nulle et dont le discriminant est un monôme multiplié par une unité sont des séries de Puiseux en plusieurs variables. Nous présenterons une généralisation de ce résultat pour les polynômes dont le discriminant est un polynôme quasi-homogène multiplié par unité. Nous rappellerons la construction de Newton-Puiseux pour la construction des racines d'un polynômes à coefficients dans le corps des racines en une variable.
According to Shub and Smale's tau-conjecture, the number of integer roots of a univariate polynomial should be polynomially bounded in the size of the smallest (constant free) straight-line program computing it. This statement becomes provably false if one counts real roots instead of integer roots. I have proposed a real version of the tau-conjecture where the attention is restricted to straight-line programs of a special form: the sums of products of sparse polynomials. This conjecture implies that the permanent polynomial cannot be computed by polynomial-size arithmetic circuits. The complexity of the permanent in the arithmetic circuit model is a long standing open problem, which can be thought of as an algebraic version of P versus NP. In this talk I will present the real tau-conjecture and its consequence for the permanent. If time allows, I will introduce a new tool in this context: the Wronksian determinant. This leads to some modest progress on the real tau-conjecture, and to new bounds on the number of solutions of sparse systems of polynomial equations. The latter bounds seem to be of independent interest from the point of view of real algebraic geometry.
Dans un travail antérieur avec Damien Pous, on définit une sémantique pour CCS, qui peut être vue à la fois comme une sémantique de jeux non-déterministe et comme une sémantique de préfaisceaux innocents. Les résultats d'adéquation obtenus pour cette sémantique reposent sur le fait que les parties du jeu forment une catégorie fibrée, au sens de Grothendieck, au-dessus des positions. On s'attaque ici à poursuivre notre approche dans le cadre du pi-calcul. Or, s'il est facile de concevoir un jeu pour pi dans l'esprit de celui pour CCS, il est beaucoup moins évident que les parties sont fibrées au-dessus des positions. On montrera qu'elles le sont, en utilisant un outil catégorique bien connu: les systèmes de factorisation.
La croissance de bulles influence le type d'éruption volcanique et est à la base de l'étude du dégazage volcanique. Lors des éruptions effusives les bulles forment par coalescence un chemin vers la surface qui permet au gaz de s'échapper. Au contraire lors d'éruptions explosives les bulles de gaz n'ont vraisemblablement pas réussi former ce chemin. Dans un premier temps nous décrivons et étudions la croissance d'une bulle moyenne représentative par le couplage de deux e.d.o. et d'une e.d.p. Cette étude souligne les limites de cette modélisation microscopique. C'est pourquoi, ensuite, nous proposons une modélisation statistique qui décrit l'évolution d'une population de bulles de tailles différentes en interaction. Plusieurs problèmes sont a résoudre, comme la définition de l'interaction entre bulles, des taux de croissance et leurs simulations. Ces travaux sont le fruit d'une collaboration inter-disciplinaire dans le cadre de l'ERC DEMONS
Je vais présenter un travail en commun avec A. Chambert-Loir dans lequel nous développons, dans le cadre analytique p-adique, et plus précisément dans celui des espaces de Berkovich, un formalisme de type 'formes et courants' ressemblant à celui qui existe en géométrie complexe : nous définissons des formes de type (p,q), l'intégrale d'une forme de type (n,n) et l'intégrale de bord d'une forme de type (n-1,n) (où n est la dimension de l'espace ambiant) ; nous prouvons l'analogue de la formule de Stokes et de la formule de Poincaré-Lelong.... Nous utilisons de manière absolument cruciale une théorie des formes de type (p,q) sur R^n (que nous rapatrions ensuite dans le monde Berkovich) qui a été mise au point par Lagerberg avec des motivations tropicales ; je consacrerai une première partie de l'exposé à expliquer sa construction.
Le but de l'exposé est de faire une introduction élémentaire à l'exposé d'Antoine Ducros. Ainsi, guidé par un joli résultat de Sam Payne, nous commencerons tout d'abord par faire des rappels sur la géométrie et la topologie ultramétrique, puis nous introduirons les espaces de Berkovich et expliquerons ses liens avec la géométrie tropicale.
Il est en général indécidable de tester si une définition récursive est bien fondée, mais il existe de nombreux tests pour décider des conditions suffisantes pour la bonne fondation. Le principe du ``size-change'' de A. ben Amram, N.D. Jones et C.S. Lee est particulièrement simple (il s'agit simplement d'examiner certaines boucles dans le graphe d'appels des fonctions récursives), élégant (il repose sur le théorème de Ramsey) et puissant. C'est ce principe qui a été étendu et implanté dans le language PML. Les extensions vont dans deux directions : - autoriser la taille des arguments à augmenter localement, - utiliser la structure du langage (constructeurs / filtrage). Un point important est que ces extensions ne rendent pas le test plus compliqué à implanter.