Je ferai une présentation rallongée de l'article LICS du même nom. Il s'agit de donner une caractérisation, pour une classe importante de modèles du lambda-calcul non typé, de la pleine adéquation pour la normalisation de tête (i.e. pour H*). On montrera en effet qu'il est pour cela nécessaire et suffisant d'être hyperimmune. L'hyperimmunité est une notion que nous introduirons qui demande à ce que les comportements mal fondés du modèle ne soient pas capturables par des fonctions récursives. Ce résultat sera notamment utilisé comme prétexte et exemple pour l'introduction d'un outil central dans ma thèse: les lambda-calculs avec tests. Il s'agit d'enrichir le lambda-calcul non typé avec des opérateurs directement issus du modèle dénotationnel impliqué afin de rendre celui-ci pleinement adéquat pour notre nouvelle syntaxe. Intuitivement, ces opérateurs vont internaliser un processus d'inférence de type possiblement divergent qui tente de typer l'arbre de Böhm d'un terme.``
We investigate continuous rational maps from a compact nonsingular real algebraic variety into unit spheres. In some cases we characterize continuous maps that (a) are homotopic to continuous rational maps, or (b) can be approximated by continuous rational maps. Of course, continuous maps that satisfy (b) also satisfy (a). It remains an open problem whether the converse always holds; we show that it does under certain reasonable assumptions.
We extend the definition of Christoffel words to directed subgraphs of the hypercubic lattice in arbitrary dimension that we call Christoffel graphs. Christoffel graphs when d=2 correspond to well-known Christoffel words. Due to periodicity, the d-dimensional Christoffel graph can be embedded in a (d−1)-torus (a parallelogram when d=3). We show that Christoffel graphs have similar properties to those of Christoffel words: symmetry of their central part and conjugation with their reversal. Our main result extends Pirillo's theorem (characterization of Christoffel words which asserts that a word amb is a Christoffel word if and only if it is conjugate to bma) in arbitrary dimension. In the generalization, the map amb↦bma is seen as a flip operation on graphs embedded in ℤd and the conjugation is a translation. We show that a fully periodic subgraph of the hypercubic lattice is a translate of its flip if and only if it is a Christoffel graph.
Étant donné un polynôme f in Z[x], où x est un uplet de variables, on s'intéresse à déterminer le nombre de zéros dans l'anneau Z/mZ en fonction de m. En général, ceci est un problème difficile, mais Denef-Igusa-Meuser ont démontré que la série de Poincaré associée à f est une fonction rationelle. Ceci donne une relation (assez mystérieuse) entre les nombres de zéros dans Z/p^rZ quand p est un nombre premier fixé et r varie. Je vais donner une explication géométrique de ce résultat. L'ingrédient clé est l'existence de ``t-stratifications'' - stratifications qui, à priori, vivent dans des corps valués, mais qui induisent des stratifications de Whitney dans C et R. (En fait, les stratifications dans C et R induites par des t-stratifications sont même proche d'être des stratifications bilipschitz au sens de Mostowski.)
Nous présentons une construction algébrique qui a pour loi de composition l’unification de termes du premier ordre, et comment y représenter le calcul. La correspondance preuve-programme fournit alors une façon innovante de représenter les entiers binaires comme des fonctions dialoguant avec les programmes. Les machines abstraites que l’on peut y encoder (les observations) peuvent naturellement être vues comme des machines à pointeurs, qui parcourent l’entrée sans la modifier. On montre alors que ces observations sont suffisamment expressives pour caractériser l’espace logarithmique, et que décider de l’acceptation d’un mot par une observation est réductible au problème d’acyclicité d’un graphe, un problème également en espace logarithmique. (En collaboration avec Marc Bagnol [http://iml.univ-mrs.fr/ bagnol/], Paolo Pistone et Thomas Seiller [http://www.ihes.fr/ seiller/])
V. Kaloshin (2005) gave a method to Whitney stratify semi-algebraic sets. We correct his proof and give a more general result applying to definable sets in arbitrary o-minimal structures. (Work in collaboration with Nguyen Xuan Viet Nhan and Saurabh Trivedi.)
On s'intéresse à la modélisation des fluides supercritiques multi-espèces réactifs. Ces fluides font notamment intervenir des thermochimies non idéales et des flux de diffusion proportionnels aux gradients de potentiels chimiques. On étudie la structure du système d'équations aux dérivées partielles correspondant ainsi que la stabilité asymptotique de ces états d'équilibre. Les simulations numériques concernent les flammes d'hydrogènes transcritiques.
Dans ce travail, nous étudions la stabilisation exponentielle en dimension deux et trois des équations de Navier-Stokes dans un domaine borné Ω, autour d’un état d'équilibre donné, au moyen d'un contrôle frontière. Afin de déterminer la loi de contrôle, nous considérons un système étendu couplant les équations de Navier-Stokes avec une équation satisfaite par le contrôle sur la frontière du domaine. Alors que la plupart des approches traditionnelles appliquent un contrôle via une équation algébrique de Riccati ou via un opérateur de Stokes-Oseen par exemple, une méthode de Galerkin est proposée à la place dans cette étude. La méthode de Galerkin permet de construire le contrôle frontière et à l’aide de techniques d’estimation a priori de l'énergie, la décroissance exponentielle est obtenue. Ensuite un résultat de compacité permet alors de passer à la limite dans le système des solutions approchées.
L' Institut Camille Jordan accueillera du 19 au 23 mai 2014 le colloque Inter’Actions dédié aux intéractions entre les jeunes chercheurs et leurs domaines de recherches. Ce colloque s'intègre dans le cadre de la fédération Mathématiques Rhône-Alpes-Auvergne et tend à resserrer les liens entre les doctorants de ces différents laboratoires. Il s'agit de la deuxième edition de ce colloque qui avait eu lieu l'an dernier à Clermont-Ferrand.
Une question aussi ancienne que la programmation linéaire consiste à trouver une règle de pivotage pour l’algorithme du simplexe conduisant à un nombre polynomial d’opérations. Une autre question consiste à trouver un algorithme résolvant en temps polynomial un jeu répété déterministe dont la valeur est définie comme un paiement moyen par unité de temps. Nous montrons que la convexité tropicale permet de relier ces deux questions: une règle de pivotage satisfaisant certaines conditions techniques permettrait de résoudre les jeux répétés. Nous exhiberons enfin un lien inattendu entre l’analogue tropical du chemin central et le chemin suivi par l’algorithme du simplexe tropical, conduisant à la construction d’exemples pathologiques de chemins centraux classiques dont la courbure totale est grande. Cet exposé présente des travaux récents avec Allamigeon, Benchimol, et Joswig, voir notamment arXiv:1308.0454, arXiv:1309.5925). Il s’appuie sur un travail avec Akian et Guterman (arXiv:0912.2462, IJAC 2012).
La ``range property'' a été conjecturée par Böhm en 1968 et a résisté 16 ans avant d'être prouvée pour quelques théories du $lambda$-calcul. En 2007, A. Polonsky a montré que la conjecture est fausse pour la théorie $H$. Je présenterai dans cet exposé des conditions nécessaires pour que cette propriété soit vraie pour la théorie $H$. Je donnerai ensuite quelques pistes pour des extensions de ces résultats à d'autres systèmes.
We propose an abstract framework for modeling state-based systems with internal behavior as e.g. given by silent or $epsilon$-transitions. Our approach employs monads with a parametrized fixpoint operator $dagger$ to give a semantics to those systems and implement a sound procedure of abstraction of the internal transitions, whose labels are seen as the unit of a free monoid. More broadly, our approach extends the standard coalgebraic framework for state-based systems by taking into account the algebraic structure of the labels of their transitions. This allows to consider a wide range of other examples, including Mazurkiewicz traces for concurrent systems. This is joint work with Filippo Bonchi, Stefan Milius and Alexandra Silva.
Given a set E in a complex space and a point p in E, there is a unique smallest complex-analytic germ containing the germ E_p, called the holomorphic closure of E at p. The variation of holomorphic closure along E may be regarded as a measure of how much the set E is 'twisted' from the point of view of the ambient complex structure. Of particular interest is the situation when E is real-analytic (or, more generally, semianalytic). In this talk, we will explain the relevance of holomorphic closure to the so-called CR geometry (a branch of modern complex analysis). We will also discuss the possibility of taming the holomorphic closure structure and its particularly nice behaviour on arc-symmetric semialgebraic sets.
Dans cet exposé, nous étudierons un modèle mathématique de corrosion. L'étude d'un tel modèle est un enjeu important puisque les phénomènes de corrosion interviennent par exemple au coeur des centrales nucléaires ou dans le stockage de déchets radioactifs. Le modèle étudié est un modèle de dérive-di usion. Par rapport au modèle de dérive-di usion ``classique'' utilisé dans la modélisation des semi-conducteurs, l'originalité de ce modèle de corrosion tient dans ses conditions limites. En eff et il s'agit de conditions de type Robin qui induisent un couplage supplémentaire fort des équations. Apres avoir décrit le modèle, nous montrerons comment obtenir l'existence de solution au niveau continu, puis nous étudierons la convergence d'un schéma volumes fi nis.
Je présenterai dans cet exposé un travail en collaboration avec Pierre Raphaël. Je m'intéresse à l'équation du flot de la chaleur harmonique, qui est la partie dissipative de l'équation de Landau Lifshitz. Certaines considérations physiques permettent de fixer comme cadre ``raisonnable'' de travail des applications du plan vers la sphère en dimension 3. Le problème dans un cadre général est encore très mal compris. C'est pourquoi on ne considère que des solutions ayant une symétrie importante, appelées solutions k co-rotationnelles, où k est le degré d'homotopie de la solution. Cette symétrie est préservée par le flot. Pour k>= 2, l'existence globales des solutions a été démontrée en 2008 par Guan, Gustafson, Nakanishi et Tsai. Avec Pierre Raphaël, nous avons obtenu une description fine de l'explosion en temps fini dans le cas de solution 1 co-rotationnelle, avec notamment, l'existence d'un ensemble discret de vitesses de concentration. De plus, pour la vitesse la plus lente, nous avons prouvé la stabilité du régime pour des perturbations de faible énergie, les autres vitesses correspondant à des états de plus en plus instables. Ainsi, après une longue présentation du problème, je montrerai comment la construction de la solution approchée permet d'obtenir les différentes vitesses d'explosion. Ensuite, je donnerai un argument formel permettant de comprendre l'instabilité du régime pour des vitesses élevées.
Le but de cet exposé est de montrer que sous certaines hypothèses, pouvant être comparées à celles du théorème d'inversion locale, l'inverse d'une application analytique par arcs d'un ensemble algébrique réel dans lui-même est encore analytique par arcs. La première étape consiste à démontrer une version du lemme clé de Denef-Loeser pour la formule de changement de variables motivique qui satisfait nos conditions. Le reste de la preuve repose essentiellement sur le polynôme de Poincaré virtuel de McCrory-Parusinski et de Fichou.
We study temporal properties over infinite binary red-blue trees in the setting of constructive type theory. We consider several familiar path-based properties, typical to linear-time and branching-time temporal logics like LTL and CTL*, and the corresponding tree-based properties, in the spirit of the modal mu-calculus. We conduct a systematic study of the relationships of the path-based and tree-based versions of eventually always blueness '' and mixed inductive-coinductivealmost always blueness'' and arrive at a diagram relating these properties to each other in terms of implications that hold either unconditionally or under specific assumptions (Weak Continuity for Numbers, the Fan Theorem, Lesser Principle of Omniscience, Bar Induction).
Joint work with Marc Bezem and Tarmo Uustalu.