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.
La théorie des pavages par tuiles de Wang a été inventée par (surprise) Hao Wang afin de proposer un problème combinatoire concret correspondant au pouvoir d'expressivité d'un fragment de la logique du premier ordre. La théorie des pavages s'est en fait révélée comme une théorie élégante s'exprimant facilement logiquement, et a ainsi apporté de nombreux résultats en logique mathématique.
Il s'agit dans cet exposé de proposer une présentation des liens entre pavages et logique. On analysera en particulier comment deux des théorèmes fondamentaux sur les pavages se traduisent :
- Par l'existence d'une théorie complète finiment axiomatisable et superstable [Makowsky, Poizat]
- Par le fait que le fragment AEA de la logique du premier ordre forme une classe de réduction conservative [Büchi, Kahr-Moore-Wang]
tout en expliquant bien entendu ce que signifient les nombreux mots potentiellement obscurs des phrases précédentes.
Aucune connaissance sur les pavages n'est nécessaire. Une connaissance rudimentaire de la logique du premier ordre sera appréciée.
Les exceptions sont généralement vues comme un mécanisme modifiant le flot de contrôle d'un programme. Cette vision cantonne les exceptions aux langages pour lesquels la notion de flot de contrôle est bien définie, ce qui n'est généralement pas le cas pour les langages de la théorie des types. Nous présenterons un mécanisme où les exceptions sont attachées aux valeurs plutôt qu'au flot de contrôle, ainsi qu'un système de types pour ces exceptions basé sur la notion de corruption. Nous montrerons que cette notion, utilisée à travers une relation de sous-typage, permet la détection statique d'exceptions non rattrapées, et ce sans compromettre la propagation automatique des exceptions. Nous illustrerons ce système d'exceptions dans le cadre d'une extension du Système F, utilisé ici comme une première étape vers des systèmes de types plus riches (avec pour horizon le calcul des constructions). Enfin, nous présenterons un modèle de réalisabilité pour justifier et expliquer la notion de corruption dans notre calcul.
La représentation des images par des descripteurs géométriques locaux s'est imposée dans nombre d'applications comme la détection d'objets, l'identification de scène, la reconstruction 3D, la création de panorama, etc. Ces descripteurs sont généralement construits autour de points d'intérêt, par exemple sous la forme d'histogrammes locaux d'orientation du gradient de l'image (cas des descripteurs SIFT proposés par D. Lowe), ce qui leur permet d'être invariants ou robustes à de nombreuses transformations et altérations de l'image. Dans cet exposé, on s'intéresse à l'appariement de tels descripteurs. Pour chaque descripteur d'un ensemble de requêtes, on souhaite décider s'il ressemble ou non à certains descripteurs d'une base de données. Dans la littérature, cette étape se résume souvent au choix d'un seuil sur la distance euclidienne au plus proche voisin. La procédure de mise en correspondance que nous proposons utilise d'une part une distance de transport entre descripteurs et d'autre part une approche a contrario qui permet de valider ou pas les mises en correspondance. Cette approche fournit des seuils de validation qui s'adaptent automatiquement à la complexité de chaque descripteur requête et à la diversité de la base de données. Elle permet à la fois de détecter plusieurs occurences d'une même requête et de gérer correctement les cas où aucune de ces requêtes n'est présente dans la base de données. Aux appariements ainsi validés correspondent des transformations dans le plan des images. La détection de groupes spatialement cohérents dans l'espace de ces transformations permet in fine de reconnaître des ``formes globales'' entre les images considérées.