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.
Le project MathLang a pour but de computeriser des textes de mathematiques selon des degres de formalisation differents, et sans preciser d'avance un engagement dans:
* un logique particulier (par example, sans devoir choisir comme base une theorie des ensembles, une theorie des categories, une theorie des types, etc.)
* un systeme de demonstration particulier (par example, sans devoir choisir comme systeme de demonstration Mizar, Isaeblle, Coq, PML, etc.).
MathLang laisse les choix concernant les systemes de demonstration et de la logique ouverts tant que c'est possible. En plus, MathLang permet des niveaux varies de computerisation, et n'insiste pas qu'une formalisation soit complete comme c'est fait dans les fondations de la mathematiques a la Russell et Frege ou dans les systemes de demonstration (comme initie par de Bruijn). Pendant la computerisation, le text mathematique est d'abord insere dans l'ordinateur tel qu'il est ecrit par le mathematicien sur papier. Puis un ou plusieures aspets de MathLang sont appliques au texte pour donner des versions du texte qui sont (automatiquement) controles a des niveaux differents:
1. Un aspect de base est l'extension du texte avec l'information categorique (terme, nom, adjectif, proposition, etc) ou la coherence et la structure grammaticale du texte sont controlees automatiquement.
2. Un autre aspect partage le texte en parties annotees par des relations (e.g., Corollaire A utilise Theorem B) et automatiquement controle la structure logique du texte (ce n'est la correction logique du texte).
3. Un autre aspect transforme le texte alors que les trous dans les preuves sont evidents.
4. D'autres aspects transforment cette version derniere en une formalisation complete (dans Coq, Mizar, Isabelle, etc).
MathLang a ete cree par Fairouz Kamareddine et J.B. Wells en 2000. Nous avons computeriser des textes dans MathLang (pas a pas) jusqu'a des formalisations completes dans Coq et Mizar (aussi Isar/Isabelle). Depuis 2002, 4 etudiants de theses (Manuel Maarek, Kryztof Retel, Robert Lamar et Christoph Zengler) et des dizaines d'etudiants de master et de BSc ont contribue au design et a l'implantation de MathLang et a son utilisation pour la computerisation des textes de Maths.
S'il reste du temps, Fairouz pourra enchaîner sur un exposé plus orienté lambda-calcul:
Titre: Parametres dans le lambda calcul type.
Les fonctions dans le lambda calcul sont toujours d'ordre superieur. Traditionellement, les fonctions en maths sont d'ordre inferieur. Ici, on donne le lambda calcul avec des fonctions d'ordre inferieur et on divise le cube de Barendregt en 8 sous-cubes qui permettent des meilleures representations des constructeurs dans les languages ML, LF et Automath.
C'est un travail commun avec Twan Laan et Rob Nederpelt.