I report on work in progress concerning the development of a natural language parser. On the one hand I discuss how a call-by-value lambda-mu-calculus endowed with labels can be used to provide a Montague semantics for natural language and how events can be exploited in order to deal with linguistic phenomena such as adverbs. On the other hand I explain how a type-driven parser can be obtained by enriching the type system with morphosyntactic and grammatical features.
Les automates cellulaires sont souvent construits et étudiés pour adopter un comportement précis. On adopte ici un point de vue opposé en s'intéressant aux comportements typiques parmi l'ensemble des AC ou de manière équivalente au comportement des AC aléatoires. A l'aide de méthodes combinatoires variées, et de la complexité de Kolmogorov, on obtient des résultats sur la probabilité de certaines propriétés dynamiques des AC.
Comessatti a démontré qu'une surface rationnelle réelle est soit non orientable, soit difféomorphe à une sphère ou un tore. Réciproquement, si S est une surface non orientable ou difféomorphe à une sphère ou un tore, il existe une surface rationnelle réelle X difféomorphe à S. Dans cet exposé on démontre que si Y est une autre surface rationnelle réelle difféomorphe à S, alors X et Y sont biregulièrement isomorphes. Autrement dit, les surfaces non orientables, la sphère et le tore ont exactement un seul modèle algébrique rationnel réel à isomorphisme birégulier près.
Le travail présenté introduit une nouvelle approche pour la composition automatique de buts en planification en considérant les buts comme des fonctions de leur contexte (i.e., à partir de structures de connaissances sur le domaine). Etant donné un but global et une situation initiale, le modèle de planification peut être généré directement à partir d'un ensemble de buts primitifs via la connaissance du domaine et le raisonnement sur les types de buts. La connaissance sur le domaine est extraite d'une ontologie locale, sélectionnant les entités disponibles et leurs relations. Un processus de raisonnement valide ces informations via un theorem prover en théorie intuitionniste des types (ITT). L'approche proposée bénéficie de l'efficacité du theorem prover à travers ITT combinée à l'expressivité sémantique des ontologies. La representation des connaissances utilise les types d'enregistrements dépendants pour décrire à la fois les types de contextes du domaine et des structures intentionnelles décrivant une action, le but à réaliser et ses effets. Les types d'enregistrements dépendants capturent une connaissance partielle du domaine et possèdent un impact computationnel immédiat.
Cet exposé traitera de l'existence de solutions fortes pour Navier-Stokes compressible isotherme dans des espaces de Besov critiques pour le scaling du système. On montrera notamment l'existence de solutions fortes pour des données à indices de régularité négatifs. De plus cet exposé fera un lien avec le système de type Korteweg c'est à dire avec un terme de capillarité.
On borne le nombre de points fixes d'un automorphisme d'une courbe algébrique réelle en fonction du genre de la courbe et du nombre de composantes connexes de la partie réelle de la courbe. On utilise cette borne pour calculer l'ordre maximum de certains groupes d'automorphismes de courbes algébriques réelles.
Dans le cadre du pi calcul, la bisimulation ouverte est une notion d'équivalence attractive car elle offre de bonnes propriétés de congruence et est assez facile à implémenter. Nous proposons une généralisation de cette notion dans le cadre du spi calcul, une extension du pi calcul permettant de raisonner sur les protocoles cryptographiques.
When enriching the lambda-calculus with rewriting, union types may be needed to type all strongly normalizing terms. However, with rewriting, the elimination rule (UE) of union types may also allow to type non normalizing terms (in which case we say that (UE) is unsafe). This occurs in particular with non-determinism, but also with some confluent systems. It appears that studying the safety of (UE) amounts to the characterization, in a term, of safe interactions between some of its subterms. We study the safety of (UE) for an extension of the lambda- calculus with simple rewrite rules. We prove that the union and intersection type discipline without (UE) is complete w.r.t. strong normalization. This allows to show that (UE) is safe if and only if an interpretation of types based on biorthogonals is sound for it.
Une session de travail les 29, 30 Mai au sein du groupe ModCan (Modélisation Cancer) avec Bordeaux (T. Colin, O. Saut), Chambery, Grenoble (Claude Verdier), Lyon (F. Billy, Emmanuel Grenier, Benjamin Ribba), Turin (D. Ambrosi, L. Preziosi) est organisee au LAMA.
Une classe effective dans une variété symplectique de dimension quatre est une classe d'homologie de degré deux qui est réalisée par une courbe J-holomorphe (éventuellement réductible) pour toute structure presque complexe positive sur la forme symplectique. Je montrerai que les classes effectives sont orthogonales aux tores lagrangiens pour la forme d'intersection.
Nous montrerons comment un langage similaire à ML, peut être transformé de manière très simple et minimaliste en un système de déduction où les preuves sont des programmes.
On considère l'équation de Boltzmann pour un gaz à deux composantes lorque le nombre de Knudsen devient petit. Une des 2 composantes satisfait à des conditions de bord de type données aux bords rentrantes et l'autre composante satisfait à des conditions de bord de type Maxwell diffuses. La solution du problème est alors rechechée sous la forme d'un développement asymptotique de type Hilbert avec un reste contrôlé.
Soit W -> X une variété projective non singulière réelle de dimension 3 fibrée en courbes rationnelles. On suppose que W(R) est orientable. Soit M une composante connexe de W(R). D'après Kollár, M est alors essentiellement une variété de Seifert ou une somme connexe d'espaces lenticulaires. Soit n un entier définit de la façon suivante : Si g : M -> F est une fibration de Seifert, on note n le nombre de fibres multiples de g. Si M est une somme connexe d'espaces lenticulaires, on note n le nombre d'espaces lenticulaires.
Théorème
Lorsque X est une surface géometriquement rationnelle, n est majoré par 4.
Ce résultat répond par l'affirmative à une question de Kollár qui avait montré en 1999 que n était majoré par 6. On déduit ce théorème d'une analyse fine de certaines surface de Del Pezzo singulières avec singularités Du Val.