We present a new approach to the problem of static typing in languages of the ML family. The basic idea is to generalize the pseudo linear unification algorithm you can use in the Hindley-Milner algorithm. The obtained language is very expressive compared to existing ML implementation and do not require type annotation for many features of ML that usually needs some (like modules, object, ...).
Un ovale d’une courbe algébrique réelle plane est dit pair, s’il est contenu dans un nombre pair d’ovales de la courbe. En 1906, Virginia Ragsdale a conjecturé que pour toute courbe de degré 2k avec p ovales pair,
La théorie de types a été inventée au début du 20eme siècle avec le but d'éliminer les paradoxes qui viennent de l'application d'une fonction à elle-même. Le lambda calcul a été développé (par Church) vers 1930 comme une théorie de fonctions. En 1940, Church ajoutait les types à son lambda calcul. Ces types étaient simples, ce qui veut dire qu'ils n'étaient jamais construits par des lieurs (comme un $lambda$). Alors, on a des termes comme $lambda_{x:T}.B$ (qui sont construits par le lieur $lambda$) mais on n'a pas des lieurs qu'on peut utiliser pour construire un type. Malgré l'influence qu'a connue le lambda calcul typé de Church, sa limitation a aboutit a la création de plusieures théories de types dans la deuxième partie du 20eme siècle. Dans ces calculs, les types sont construits par des lieurs. Dans la plupart de ces calculs, on trouve deux lieurs : le $lambda$ (pour construire des termes) et le $Pi$ (ou $forall$, pour construire des types). Ces deux lieurs nous permettent de distinguer les fonctions (qu'on construit avec les $lambda$s) des types (qu'on construit avec les $Pi$). En plus, dans ces calculs, on permet bien la $beta$-réduction mais pas la $Pi$-réduction. Autrement dit, dans ces calculs on a bien la règle : $(lambda_{x:A}.B)C rightarrow B[x:=C]$ Mais pas la règle : $(Pi_{x:A}.B)C rightarrow B[x:=C]$ En particulier, lorsque $b$ a le type $B$, on donne à $(lambda_{x:A}.b)C$ le type $B[x:=C]$ à la place de $(Pi_{x:A}.B)C$. Il y a quelques extensions puissantes des théorie des types qui donnent le même comportement au $Pi$ qu'au $lambda$ (par exemple, en Automath, dans le langage de programmation Henk de Simon Peyton Jones, etc.). Ca nous aboutit à poser la question : pourquoi distinguer entre le $lambda$ et le $Pi$ lorsque des systèmes comme Automath nous montrent qu'il est plus avantageux de traiter les types exactement comme les termes? Dans cette présentation je décrit un système ou les deux lieurs sont identifiés et je montre que ce système a toutes les propriétés qu'on désire d'un système de typage sauf pour l'unicité des types. Mais je démontre aussi que cette perte de l'unicité des types n'est pas grave parce qu'il y a un isomorphisme entre le typage avec deux lieurs et le typage avec un seul lieur et en plus, tous les différent types d'un même terme, suivent le même modèle.
On appelle circuit tout ensemble de n+2 points entiers dans Zn. Un système polynomial est supporté par un circuit si ses n équations ont pour support commun un circuit dans Zn.
On donne ici des bornes supérieures sur le nombre de solutions réelles d’un tel système en fonction du "rang modulo 2" du circuit et de la dimension de l’espace affine du sous-ensemble minimal du circuit constitué de points affinement dépendants. On montre que ces bornes sont exactes en dessinant des graphes sur la sphère de Riemann, qui sont des exemples de "Dessins d’enfants".
On obtient aussi qu’un tel système a au plus n+1 solutions positives (dont toutes les coordonnées sont strictement positives), et cette borne est exacte. Cette dernière borne n+1 améliore considérablement la borne donnée par le théorème de Khovanskii (théorie des Fewnomials).
We will look at what is involved in formally proving results about languages with binding. We will in particular focus on what we want to prove, what we actually do prove, and what requirements we need to put on the formalisms that we use.
Je présenterai deux résultats concernant le contrôle d’une structure o-minimale par ses ensembles définissables de dimension deux :
- La structure engendrée par les sous-ensembles semi-algébriques de R2 élimine ses quantificateurs (théorème de Tarski-Seidenberg pour les ensembles semi-2-algébriques).
En particulier, il existe une structure o-minimale strictement plus petite que celle des semi-algébriques mais qui définit (exactement) TOUS les ensembles semi-algébriques de R2.
- Considérons une expansion (o-minimale) S du corps des réels qui admet un théorème de décomposition C^{infty}.
S’il existe un n>1 tel que tous les ensembles S-définissables sont en fait semi-algébriques alors S est la structure des semi-algébriques.
On peut ainsi "reconnaître" les structures qui définissent des ensembles non semi-algébriques dès la dimension 2.
Soit $(X, omega)$ une variété symplectique de dimension quatre équipée d’une involution antisymplectique $c_X$. Le lieu fixe de $c_X$ est une surface lagrangienne lisse notée $R X$. Soit $L$ une courbe lisse de $R X$ qui réalise $0$ dans $H_1 (R X ; /2)$. Je présenterai la construction d’invariants par déformation du quadruplet $(X, omega, c_X, L)$. Ces invariants sont obtenus en comptant avec signe les courbes $J$-holomorphes réelles qui réalisent une classe d’homologie donnée, passent par un nombre adéquat de points fixés et sont tangentes à $L$. Je discuterai ensuite plusieurs applications de ces résultats.
Comment caractériser les germes de fonctions indéfiniment différentiables qui sont entièrement déterminés, modulo un changement de variable lisse, par leur série de Taylor à l’origine, ou leur jet sur un fermé ? Dans le cas de germes à point critique isolé, le problème est parfaitement compris depuis les années 70 -- il s’agit en quelque sorte d’une variante "d’ordre infini" de la notion de jet suffisant (selon la terminologie de Thom) ou de détermination de germes (selon celle de Mather). Il en va autrement pour les singularités non isolées, où une caractérisation est connue seulement dans des cas très particuliers. On présentera un résultat sensiblement plus général.
Les invariants de Gromov-Witten peuvent être vus géométriquement comme les nombres de certaines courbes complexes ou pseudo-holomorphes de genre donné qui représentent une classe d’homologie donnée d’une variété donnée.
On étudie la croissance des invariants de Gromov-Witten GWnD de genre zéro du plan projectif P2k éclaté en k points, où D est une classe dans le deuxième groupe d’homologie de P2k. Sous des hypothèses naturelles sur D, on obtient l’asymptotique précise de la suite log GWnD.