La logique linéaire s'interprète dans les espaces vectoriels, même si les exponentielles posent problème (on obtient des espaces de dimension infinie). Dans le cas fini, cette interprétation est malheureusement un peu dégénérée car l'interprétation d'une formule (un espace vectoriel) est isomorphe à celle de sa négation (l'espace des formes linéaire sur cet espace). Christine a récemment proposé une solution : en plus de l'espace vectoriel, on rajoute une notion de totalité. Typiquement, une fonction linéaire de A dans B est totale ssi elle envoie les vecteurs totaux sur des vecteurs totaux. Algébriquement parlant, la totalité est un sous-espace affine de l'espace vectoriel considéré.
Christine introduira tout ça avec un peu plus de détails, et expliquera comment obtenir un premier résultat de complétude : complétude d'un calcul booléen basé sur la traduction habituelle du type Bool => Bool dans la logique linéaire. Pierre poursuivra avec un second résultat toujours de complétude : complétude d'une logique linéaire sans exponentielles. (Ça, c'est si la preuve ne « devient » pas fausse d'ici là...)
Le premier résultat ne nécessite aucune connaissance en logique linéaire (si si, c'est vrai), et le second présuppose un modicum de logique linéaire pour comprendre le pourquoi (mais pas le comment). Des connaissances de base en algèbre linéaire sont nécessaires, mais rien de compliqué, et seulement en dimension finie.
Dans le modèle des automates cellulaires, la non-linéarité est omniprésente. Une voie pour étudier ces objets peut être la théorie du chaos déterministe. Elle a déjà été largement empruntée dans la littérature (avec les travaux de P. Kurka notamment), mais pratiquement toujours en se restreignant à la dimension 1. En ce concentrant sur certaines propriétés autour de la sensibilité aux conditions initiales, nous montrerons dans une première partie de cet exposé que cette restriction n'est pas neutre : une nouvelle classe de comportements dynamiques (les automates cellulaires non sensibles aux conditions initiales mais sans point d'équicontinuité) apparaît à partir de la dimension 2. De la démonstration de l'existence de cette classe, nous tirerons d'autres résultats montrant que la complexité de certaines propriétés fait un bond lorsque l'on quitte la dimension 1.
Dans une seconde partie d'exposé, nous prendrons un peu de recul sur la question de la variation de complexité des propriétés en fonction de la dimension. Nous poserons un cadre logique formalisant ce que l'on peut appeler la ``dynamique topologique'' dans les automates cellulaires. Nous aborderons alors le problème suivant : étant donnée une propriété (une formule dans notre théorie), quel est la complexité de l'ensemble des automates cellulaires qui la satisfont ? cet ensemble est-il arithmétique ? à quelle hauteur dans la hiérarchie ? comment cette hauteur varie avec la dimension ?
Selon la vitalité de l'orateur, le traitement de ce questionnement pour aller du simple traitement d'exemples à la démonstration d'un résultat général.
Composition of strategies is the crucial operation of game semantics. It corresponds to cut elimination in proof theory. This paper is an attempt to uncover the sheaf-theoretical nature of these two operations. We define a game semantics with a topological flavor for a variant of Multiplicative Additive Linear Logic (henceforth MALL). We show that the standard notion of strategy leads to a correct, yet incomplete model. We then introduce a new, non-standard notion of local'' strategies, which turn out to form a sheaf. <br><br> Composition of strategies is generally divided into two steps: interaction, and hiding. In our setting, interaction arises as gluing in the sheaf of local strategies. Hiding along a cut c: U -> V appears here as an instance of a more general operation,descent'' along c, which also encompasses cut elimination. Descent along c is a morphism of sheaves on V from the direct image along c of local strategies on U, into cut-free local strategies on V. It arises from a factorisation system, roughly dividing plays into their cut-only and cut-free parts.
Finally, our notion of (winning) local strategy is validated by the expected soundness and completeness results w.r.t. MALL provability.
Je parlerai des zippers : leurs principes, comment ils amènent à une notion de dérivée de type de données. On verra alors une première définition de cette dérivée par McBride, quelques problèmes et une deuxième définition pour y répondre. Puis nous passerons brièvement aux containers, une notion générale de type de données. Nous verrons comment étendre la notion de dérivée aux containers pour finir sur une formule de Taylor des containers.
Nous présentons dans ce document des modèles d'écoulements bicouches. Il s'agit de modèles d'écoulement en eaux peu profondes et de modèles de transport de sédiments. Nous dérivons dans un premier temps des modèles de Saint-Venant visqueux, bicouches et bidimensionnels en supposant que l'écoulement est composé de deux fluides immiscibles (cas du détroit de Gibraltar). Nous donnons quelques résultats numériques sur les modèles visqueux dérivés. On étend alors les résultats d'existence de solutions obtenus dans le cas monocouche au cas bicouches. Dans cette analyse, la difficulté provient des termes de frottement au vu des multiplicateurs utilisés dans les estimations d'entropies. Nous proposons ensuite de nouveaux modèles de transport de sédiments énergétiquement consistants pour lesquels nous obtenons des résultats théoriques de stabilité. Enfin, nous développons une nouvelle version flux limiteur de schéma numérique volumes finis, bien équilibré, en combinant un schéma de type Roe et de Lax-Wendroff, tous deux étant construits en tenant compte de la variation tangentielle des quantités. Ce schéma numérique est utilisé pour simuler le transport de sédiment.
Dans cet exposé nous allons faire une présentation de notre code d'hydrodynamique côtière VOLNA. Tout d'abord, nous commençons par le contexte physique de cette étude qui tourne autour des tsunamis, de la simulation numérique du run-up et du couplage avec des modèles phase moyennée. Ensuite, nous passerons par une brève présentation des méthodes numériques mises en oeuvre dans notre code. Notamment, nous utilisons un schéma volumes finis d'ordre deux avec un maillage triangulaire non structuré. La complexité géométrique de la ligne côtière justifie l'utilisation de ce type de maillages. Ce schéma a été initialement développé dans le cadre des écoulements diphasiques. Mathématiquement nous résolvons pour l'instant les équations de Saint-Venant et nous travaillons actuellement sur une extension au système de Boussinesq. Finalement, nous montrerons quelques cas-tests assez réalistes pour faire preuve des perfomances du code.
Les espaces cohérents de Jean-Yves Girard et les espaces de finitude de Thomas Ehrhard sont obtenus à partir d'une base « similaire » : l'orthogonalité.
Je commencerais par rappeler comment ça marche (parce que c'est intéressant et pas très compliqué), puis je passerais à une structure mixte qui permet de générer des espaces de finitude « simples » à partir d'espaces cohérents.
Cette construction contient tous les exemples usuels d'espaces de finitude et de plus, elle commute avec les opérations logiques (⅋, ⊗, ⊕, &, ⊸, !, …) Un des aspects intéressants est l'utilisation du théorème de Ramsey infini pour démontrer certaines propriétés de cette construction.
Je finirais par expliquer comment on tombe sur une notion qui généralise les fonctions stable de Berry pour permettre d'interpréter une version simple du λ-calcul algébrique de Lionel, Thomas et consorts.
Remarques : j'essaierais, autant que possible, de ne pas supposer connue toute la logique linéaire. Les deux premiers tiers de mon exposé devraient donc être « self-contained »...
La droite réelle de Harthong-Reeb est un modèle non-standard du continu qui est à l'origine de nombreux développements en géométrie discrète (entre autre la droite discrète de Réveillès). Selon Harthong et Reeb eux-mêmes leur modèle n'est pas sans liens avec une approche constructive. Récemment à Poitiers et à La Rochelle nous nous sommes intéressés à cette question en montrant que la droite de Harthong-Reeb vérifie les axiomes de Bridges qui sont une théorie de la droite réelle constructive.
L'orateur propose un deuxième exposé, qui aura peut-être lieu l'après-midi s'il y a des volontaires :
Les méthodes de Monte-Carlo sont des méthodes statistiques basées sur l'utilisation de nombres aléatoires dans des expériences répétées. Les méthodes quasi-Monte Carlo sont des versions déterministes des méthodes de Monte-Carlo. Les suites aléatoires sont remplacées par des suites à faible discrépance. Ces suites ont une meilleure répartition uniforme dans le cube unité. Nous nous intéressons essentiellement à la discrépance (qui est une mesure de la déviation d'une suite par rapport à la distribution uniforme) et à une classe particulière de suites. Dans cette thèse, nous développons et analysons des méthodes particulaires Monte Carlo et quasi-Monte Carlo pour les phénomènes d'agglomération, en particulier pour la simulation numérique des équations suivantes : l'équation de Smoluchowski continue, l'équation de coagulation-fragmentation continue et l'équation générale de la dynamique des aérosols. Ces méthodes particulaires comportent les étapes suivantes : initialisation, discrétisation en temps (schéma d'Euler explicite), approximation de la densité de masse par un nombre fini de mesures de Dirac et quadrature d'intégration quasi-Monte Carlo utilisant des réseaux. Une étape supplémentaire de renumérotage (ou tri) des particules par masse croissante à chaque pas de temps est nécessaire pour assurer la convergence du schéma numérique. Ensuite, nous démontrons un résultat de convergence du schéma numérique pour l'équation de coagulation-fragmentation, quand le nombre des particules numériques tend vers l'infini. Tous nos tests numériques montrent que les solutions numériques calculées par ces nouveaux algorithmes convergent vers les solutions exactes et fournissent des meilleurs résultats que ceux obtenus par les méthodes de Monte Carlo correspondantes.
We present a variant of the explicitly-typed second-order polymorphic λ-calculus with primitive open existential types, i.e., a collection of more atomic constructs for introduction and elimination of existential types. We equip the language with a call-by-value small-step reduction semantics that enjoys the subject reduction property. We claim that open existential types model abstract types and module type generativity. Our proposal can be understood as a logically-motivated variant of Dreyer’s RTG where type generativity is no more seen as a side effect. As recursive types arise naturally with open existential types, even without recursion at the term-level, we present a technique to disable them by enriching the structure of environments with dependencies. The double vision problem is addressed and solved with the use of additional equalities to reconcile the two views.
Voir la page dédiée.
Les probabilités de ruine dans le modèle classique de la théorie du risque pour une compagnie d'assurance sont représentées par la formule de Pollaczek-Khintchine. Cette représentation a la forme d'une série de convolutions. L'approche consiste à faire une troncature de la série et à approcher les convolées par une quadrature de type quasi-Monte Carlo ou de type Monte Carlo.
Cours puis groupe de travail sur la réalisabilité avec Alexandre Miquel. Détails ici.
Nous présentons un théorème de transversalité dans la catégorie des stratifications régulières (C. Murolo, A. Du Plessis et D. Trotman) qui généralise et améliore un résultat de M. Goresky (1981). Nous en donnons deux démonstrations différentes en insistant sur les différences essentielles (2003, TAMS) et (2005, JLMS). Nous illustrerons par des applications à une théorie de l'homologie dont l'espace ambiant, les cycles et les cocycles sont des espaces stratifiés, introduite par Goresky (1976 thèse et 1981 TAMS) et étendue par C. Murolo (RdM 1994, T&iA 1996, thèse 97). Lors de l'exposé quelques problèmes ouverts et conjectures seront evoqués.
A geometric-combinatorial construction suggested by Gabrielov and Vorobjov (2007) allows one to approximate a set definable in an o-minimal structure, such as a real semialgebraic or sub-Pfaffian set, by an explicitly constructed monotone family of compact definable sets homotopy equivalent to the original set. This implies improved upper bounds for the Betti numbers of non-compact semialgebraic, fewnomial, and sub-Pfaffian sets.
Faut pas le dire, mais l'enseignement supérieur des sciences (à Nice?), ça marche pas top (taper Objectif70 dans Google). Faut pas le dire, mais nous, les universitaires (niçois?), on n'a pas trop le temps de s'occuper de ce problème, on est débordés. Et les autres, ministres et recteurs, gare à eux s'ils s'avisaient de se méler de nos affaires. Par exemple on ne cherche pas trop à enseigner la rigueur autrement que par la méthode dite de Léo Lacroix (``faites comme moi''), qui a largement fait ses réfutations. Ceux qui essaient de faire autrement, forcément, ils y arrivent pas du premier coup, et ils se font casser bien avant d'y arriver. Coqweb (à taper dans Google pour voir) propose une nouvelle méthode. C'est une interface web pour Coq, principalement développée par Loïc Pottier pour l’enseignement. Il permet aux enseignants de proposer des énoncés sous une forme suffisamment familière. Les étudiants sont invités à démontrer ces énoncés essentiellement en cliquant. Des indications peuvent être données en langage naturel, et dans ce cas, l’interface vérifie que l’étudiant a bien compris l’indication. On dira un peu de ce qu'il ne faut pas dire, puis on racontera comment Coqweb marche bien et ce qu'on a fait avec.