Cette thèse porte sur l'étude théorique et pratique d'un système de typage appliqué à la preuve de programmes de style fonctionnels. Le système de base est le système ST développé par C.Raffalli; il comporte, outre le polymorphisme, du sous-typage et de l'omission de contenu algorithmique. Nous étudions tout d'abord les modèles de la théorie définie par le système de types en se basant sur des treillis complets comportant des propriétés additionnelles permettant d'interpréter types et termes;puis nous étudions diverses propriétés théoriques du système telles que la réduction du sujet ainsi que son expressivité à travers des exemples traitant de la possibilité ou de l'impossibilité de définir des notions-clés de la logique et de l'informatique théorique. Dans la suite de la thèse, plus appliquée, nous étudions des codages de types de données riches issus de l'informatique dans le Lambda-Calcul, et montrons qu'ils s'intègrent harmonieusement dans le système; la méthodologie développée dans cette partie permet d'étendre le langage de types et le langage de programmation en conservant un critère de consistance assurant la sûreté du code typé.
On propose une notion de modèle pour la logique intuitionniste, qui étend celle fondée sur les algèbre de Heyting. Cette notion de modèle permet de distinguer l'équivalence logique (si A est démontrable, alors B aussi, et vice-versa) de l'équivalence calculatoire (toute démonstration de A est une démonstration de B, et vice-versa), ce que ne permettaient pas de faire les algèbres de Heyting. On montre ensuite que cette notion de modèle peut être utilisée pour démontrer la normalisation des démonstrations dans de nombreuses théories comme l'arithmétique de Peano ou la logique d'ordre supérieur.
On considérera la distance associée à la norme de Bombieri sur l'ensemble des polynômes homogènes réels de degré d à n variables. On montrera que si le niveau P=0 est lisse et extremal (on ne peut pas ajouter de composante à P=0 sans changer le degré) alors la distance au discriminant réel (l'ensemble des polynomes Q réels avec au moins une singularité réelle) est min{ |P(x)| ; x dans S^{n-1}, x point critique de P} On en déduira une inégalité entre la taille des composantes connexes de P=0 et la distance au discriminant.
JERA (Journées EDP Rhone Alpes) A Saint-Etienne
Le nombre de courbes algébriques complexes nonsingulières de degré d passant par d(d+3)/2 - t points et tangentes à t droites est (2(d-1))^t (si la configuration est générique et t<2d-1). F. Ronga a montré que pour une droite (t=1) le problème réel correspondant était maximal: il existe une configuration générique de points réels et d'une droite réelle telle que 2(d-1) courbes de degré d passent par les points et sont tangentes a la droite. En utilisant la géométrie tropicale on montre la maximalité de ce problème énumératif réel pour deux droites (t=2).
In this talk we present a categorical proof theory for a logic for pragmatics. The aim of this logic is to provide a framework that allows to formalize reasoninig about the pragmatic force with which a sentence may be uttered. The concept of pragmatic force comes from speech act theory and plays a crucial role also in certain branches of artificial intelligence, in particular in the developement of communication protocols for software agents. Instead of considering the full-blown theory of speech acts we focus here on speech acts that either have the pragmatic force of an assertion or the pragmatic force of an obligation, and on how these speech acts can be related to each other. In particular, we are interested in a principle proposed by Bellin and Dalla Pozza that allows the propagation of obligations through causal chains of assertions. The study of such principles from the point of view of categorical proof theory is a nontrivial task and we discuss some of the issues that need to be considered in order to get soundness and completeness results.
L'équation de Benjamin-Ono décrit la propagation d'ondes longues uni-directionnelles se propageant à l'interface entre deux fluides incompressibles non visqueux. Après avoir expliqué les motivations physiques de ce modèle, on s'intéressera aux divers approches développées pour résoudre le problème de Cauchy associé.
Dans $R^n$, avec une distribution algébrique donnée, on définit le gradient horizontal d'un polynôme, la projection du gradient de ce polynôme sur la distribution. On va donner (si le temps le permet) - quelques propriétés de base du gradient horizontal, - des exemples montrant que + longueur de trajectoires de gradient horizontal n'est pas forcément bornée, + des trajectoires de gradient horizontal peuvent avoir de cycles limites, - sous certaines conditions de généricité, par un changement de métrique, on peut montrer que longueur de trajectoires de gradient horizontal est bornée et que les trajectoires possèdent de limites.
L'effet de la structure discrète d'un milieu a petite échelle sur les ondes non linéaires qui s'y propagent est pris en compte dans un nombre croissant de modèles. Un effet du a la discrétisation peut etre le piegeage d'oscillations non linéaires autour de quelques sites d'un réseau. Un cadre mathématique pour mieux comprendre ce phénomène est l'étude des ``breathers'' (oscillations périodiques en temps et spatialement localisées) dans des réseaux d'oscillateurs non linéaires couplés. Nous examinons ce problème pour le modèle de Fermi-Pasta-Ulam, qui consiste en une chaine (ici infinie) de particules en interaction non linéaire, le couplage étant limité aux deux premiers voisins. L'existence de breathers dans ce système a ete suggerée il y a une trentaine d'années par Tsurui, en se ramenant (à partir de développements multi-echelles formels) à une équation de Schroedinger non lineéire en dimension 1. Mais cette approximation correspond-elle a des solutions exactes ? Nous verrons que cette question conduit à étudier des itérations d'applications en dimension infinie, dont la partie linéaire est un opérateur non borné, mais dont la dynamique locale est de dimension finie grace a de bonnes proprietes spectrales.
Conway a grandement participé à l'élaboration de la théorie des nombres surréels et à la théorie des jeux à deux personnes. Rapidement, un nombre surréel peut-être vu comme un jeu (potentiellement infini) très inintéressant. À cause de cette différence, les deux théories se sont depuis développées de manière quasi indépendante. Je présenterais d'abord le noyau commun aux nombres surréels et aux jeux. Ceci expliquera notamment comment il est possible d'obtenir la moitie d'un coup d'avance sur son adversaire. (Obtenir un tiers de coup d'avance est nettement plus complexe !) Je passerais ensuite à la théorie des jeux impartiaux (style Nim) dont la théorie, plus ancienne, est comprise dans la précédente. Le but est de présenter (prouver ?) le théorème de Sprague-Grundy ainsi que la conjecture sur les jeux octaux. Si le temps et l'assistance le permettent, je présenterai les avancées récentes autour des jeux impartiaux où l'on inverse gagnant et perdant (convention de 171 misère 187). Pour les survivants, je pourrais même parler (peut-être pendant le repas) de la catégorie de jeux due à André Joyal : c'est probablement la toute première catégorie monoidale close de jeux / stratégies. (Malheureusement, elle ne permet pas de modéliser la logique linéaire...) Je ne présenterais rien de nouveau dans cet exposé. Il s'agit en quelque sorte d'une publicité vantant les joies insoupçonnées de la combinatoire des jeux. Idéalement, une ou deux personnes auront envie de m'accompagner pour aller regarder un peu plus loin...
On étudie les deux limites dans le systèmme de Born- Infeld, ou le paramètre est interpreté comme le champ électrique maximal dans la théorie électromagnétique et le paramètre nul correspond à la théorie des cordes. Les deux limites sont décrites par les équations de Maxwell classiques et le système MHD sans pression. On donne les relations entre ces limites et les limites des champs forts et faibles de Brenier. Enfin, on justifie ces limites pour les solutions entropiques dans L∞ en une dimension d’espace, en utilisant des arguments de compacité et des techniques à des systèmes Lagrangiens linéaires.
L'exposé comprendra trois parties : 1) Presentation du résultat de Mikhalkin (``Real Algebaric Curves, the Moment map and Amoebas'', Ann. of Math. (2) 151 (2000)) 2) Petit état de l'Art sur les déformations (lissifications) de germes de courbes planes réelles. 3) Déformations de Harnack : définition, existence, unicité du type topologique (travail en commun avec Pedro Gonzaléz Pérez) ; quelques considérations métriques (volume de l'Amibe, taille des ovales..)
Nous chercherons à comprendre la preuve de forte normalisation du lambda calcul simplement typé (et de certaines extensions : système T de Godel, ajout d'un produit, ...) faite par Gandy. Il semble que cette preuve utilise une mesure (entière ?) qui décroit par réduction.
On fera le point sur les travaux récents, concernant l'équation de Boltzmann dans le cas homogène et avec des noyaux singuliers. On s'intéressera en particulier au problème de la régularité des solutions.
Attention: l'exposé aura lieu dans l'amphithéâtre Nivolet
Les représentations graphiques des preuves de la logique linéaire, les proof-nets, permettent de s'abstraire de contraintes inhérentes au calcul des séquents comme la syntaxe et les règles structurelles. La correction (ou prouvabilité) de tels réseaux peut se vérifier à l'aide de critères purement graphiques, comme le critère de Danos-Regnier. Sa simplicité en fait le rend très efficace mais peu compréhensible. Pour donner une preuve de complétude d'un tel critère et tenter de l'expliquer, nous utiliserons une logique différente : MILL. Dans ce système intuitionniste, les règles logiques sont des règles de typage d'un lambda-calcul et les réseaux de preuves ses arbres de syntaxe. Le critère de Danos-Regnier nous permettra de construire un lambda-terme typable à partir du réseau de preuve, assurant ainsi sa validité.
Les matériaux ferromagnétiques sont des aimants permanents. Ce type d'objets intervient dans de nombreuses applications (des télécommunications à l'enregistrement magnétique). Pour modéliser leur comportement, on utilise la théorie du micromagnétisme introduite par W.-F. Brown dans les années 60. Dans cet exposé, nous présenterons des résultats théoriques sur les propriétés des solutions des modèles du micromagnétisme ainsi qu'une chaîne de calcul permettant de comparer résultats expérimentaux et simulations numériques.
On sait bien qu'un polynome en une variable du type x^d+c avec c réel non nul possède au plus deux racines réelles non nulles alors qu'il possède d racines complexes. Plus généralement, la règle de Descartes implique qu' un polynome réel en une variable avec m+1 monomes distincts possède au plus 2m racines réelles non nulles. En particulier, si le degré d'un tel polynome est grand (par rapport à son nombre de monomes), seulement peu de ses racines complexes sont en fait réelles. En 1980 Askold Khovansky a montré qu'un tel phénomène n'était pas propre aux polynomes en une variable. Il a proposé une borne sur le nombre de solutions réelles (à coordonnées non nulles) d'un système de n équations polynomiales en n variables qui ne dépend que du nombre total de monomes distincts du système. Néanmoins, cette borne parait extremement large. Par exemple, lorsque le système est un système formé de 2 polynomes en 2 variables et avec au plus 5 monomes au total, le borne de Khovansky est 5184. Dans cette exposé, on présentera de nouvelles bornes fewnomiales obtenues très récemment avec Frank Sottile. Ces bornes améliorent considérablement celles de Khovansky. Dans notre exemple précédent, la nouvelle borne est 15. La preuve de ces nouvelles bornes est différente de celle de Khovansky (basée sur une induction sur le nombre de monomes). On se ramène à un autre système (système de Gale) en utilisant une base pour l'ensemble des relations sur les exposants du système initial. Puis, on majore le nombre de solutions réelles du nouveau système en utilisant un peu de géométrie différentielle, de la géométrie torique et de la combinatoire de polytopes.