The seminar of the team LIMD is under the responsibility of Sebastien Tavenas.
Settings: See with increasing date . Hide abstracts
Other years: 2005, 2006, 2007, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017, all years together.

Year 2008

Thursday 18th December 2008 at 10h15 Mark Weber (PPS, Paris 7),
Monads with arities

Abstract: (Hide abstracts)
A ``monad with arities'' is a monad T on some category K together with some extra data expressing the basic ``shapes'' of the operations involved in the structure of a T-algebra. There is a general result, called the nerve theorem, which in the case where K is a presheaf category, shows that the notion of monad with arities is an efficient reformulation of the notion of ``limit sketch''. The nerve theorem is so named because it generalises the characterisation of the simplicial sets that arise as nerves of categories. Other interesting instances of this result relevant for higher dimensional algebra involve ``local right adjoint monads'' -- such a T comes with a canonical choice of arities. These examples formalise the passage between the operadic and simplicial approaches to higher category theory.

Thursday 11th December 2008 at 10h15 Geneviève Paquin (LAMA),
Etude des points fixes sous la fermeture pseudopalindromique itérative

Abstract: (Hide abstracts)
Parmi les nombreuses suites remarquables étudiées en combinatoire des mots figurent les suites sturmiennes. Elles interviennent dans plusieurs domaines: dynamique symbolique, géométrie discrète, astronomie, cristallographie, etc. Elles sont d'autant plus remarquables par le fait qu'elles possèdent plusieurs caractérisations équivalentes. Entre autres, elles décrivent les droites discrètes de pentes irrationnelles. Parmi ces droites, la classe des (demies) droites passant par l'origine, appelées des suites sturmiennes standards, admet une caractérisation supplémentaire: il est possible de les construire en utilisant la fermeture palindromique itérative. La fermeture palindromique d'un mot fini w consiste à trouver le mot palindromique le plus court ayant comme préfixe le mot w. La fermeture palindromique itérative d'un mot fini w, noté Pal(w), est définie par Pal(a)=a et Pal(w)=(Pal(w_0...w_{n-1})w_n)^+, où u^+ désigne la fermeture palindromique et a est une lettre de l'alphabet. Ainsi, à tout mot sur un alphabet à 2 lettres, on peut lui associer une suite sturmienne standard en appliquant l'opérateur de fermeture palindromique itérative. Plus récemment, cette notion a été généralisée à des pseudopalindromes, c'est-à-dire des mots restant stables non pas sous l'opération d'image miroir, mais plutôt sous l'action d'un antimorphisme involutif.

D'autre part, certaines suites points fixes sous un opérateur se sont révélées être bien mystérieuses; il suffit de penser au célèbre mot de Kolakoski K=221121221221121122... qui est le point fixe sous l'opérateur de codage par blocs (le mot est égal à ses longueurs de blocs de lettres: ``2'' lettres 2, ``2'' lettres 1, ``1'' lettre 2, ``1'' lettre 1, ...). Plusieurs propriétés combinatoires de ce mot sont encore inconnues: la fréquence des lettres, la récurrence des facteurs, la fermeture de l'ensemble de ses facteurs sous l'image miroir et la complémentation, etc.

Ainsi, avec D. Jamet et G. Richomme, nous nous sommes intéressés à l'étude des points fixes sous l'opérateur de fermeture pseudopalindromique itérative. Dans mon exposé, je vais présenter certains de nos résultats concernant les propriétés combinatoires de ces mots et faisant intervenir entre autres des développements en fractions continues et des morphismes. Je terminerai en proposant certains problèmes ouverts concernant l'algébricité de la ``pente'' de certains de ces points fixes et l'existence d'exposants critiques.

Abstract available as a PDF file.

Thursday 4th December 2008 at 10h Choco (TBA),
Séminaire Choco

Abstract: (Hide abstracts)
Voir la page dédiée.

Thursday 27th November 2008 at 10h15 Damiano Mazza (LIPN, Villetaneuse),
Réécriture, catégories d'ordre supérieur, et expressivité des modèles de calcul concurrent

Abstract: (Hide abstracts)
Un problème fondamental dans la comparaison de différents modèles du parallélisme et de la concurrence est celui de définir la notion de codage, ou de traduction. A ce jour, parmi toutes les notions universellement acceptées de codage entre modèles concurrents, il n'en existe aucune qui s'impose nettement sur les autres. Nous proposons d'étudier la notion de codage en partant de la vision du calcul comme réécriture, et en utilisant des notions venant de la théorie des catégories d'ordre supérieur et de la théorie des structures d'évenemments de Winskel.

Thursday 20th November 2008 at 10h15 Ugo Dal Lago (Bologne),
Taming Modal Impredicativity: Superlazy Reduction

Abstract: (Hide abstracts)
Pure, or type-free, linear lambda calculus is Turing complete once reduction is considered as computation. We introduce modal impredicativity as a new form of impredicativity causing reduction to be problematic from a complexity point of view. Modal impredicativity occurs when, during reduction, a residual of a box b interacts with the body of another residual of b. Technically speaking, superlazy reduction is a new notion of reduction that allows to control modal impredicativity. More specifically, superlazy reduction replicates a box only when all its copies are opened. This makes the overall cost of reducing a (linear) lambda-term finite and predictable. Specifically, superlazy reduction applied to any pure proof nets takes primitive recursive time. Moreover, any primitive recursive function can be computed by a lambda-term via superlazy reduction.

Thursday 13th November 2008 at 10h15 Luigi Santocanale (LIF, Marseille),
Outils algébriques pour les logiques modales de point fixe

Abstract: (Hide abstracts)
Dans cet exposé, nous allons d’abord présenter les logiques modales plates de point fixe (flat modal fixpoint logics). Chaque logique de ce type est une extension de la logique modale K et, au même temps, un fragment du $\mu$-calcul modal propositionnel. Nous aborderons le problème de trouver, de façon uniforme, une axiomatisation de ces logiques qui soit complète par rapport à leur interprétation standard sur les modèles de Kripke.

Nous verrons comme certaines idées de l’algèbre, de la coalgèbre, et de la théorie des catégories, sont fondamentales pour notre but: la dualité, par la notion de modalité de couverture, les adjoints, avec la généralisation aux O-adjoints, les objets libres, la notion de point fixe constructif, les rétractés. Ainsi, nous serions en mesure de proposer une axiomatisation complète pour chaque logique plate de point fixe. (Travail en collaboration avec Yde Venema).

Thursday 6th November 2008 at 10h Choco (IML, LAMA),
Séminaire Choco

Abstract: (Hide abstracts)
Voir la page dédiée.

Thursday 23rd October 2008 at 10h15 Christophe Raffalli (LAMA),
PML, où en est-on ?

Abstract: (Hide abstracts)
Je dirai où en est PML, notamment, l'algorithme de typage et le proof-checking. Je montrerai les premiers exemples de programmes prouvés en PML.

Thursday 16th October 2008 at 15h15 Katarzyna Grygiel (Jagiellonian University, Cracovie),
Quantitative approach to lambda calculus

Abstract: (Hide abstracts)
The aim of this talk is to present the problem of enumerating terms in untyped lambda calculus. The very first idea was to compute the asymptotic density of strongly normalizing closed lambda terms among all closed terms of a given size. However, the preliminary task of counting lambda terms turned out to be already non-trivial and challenging and this is therefore as the main theme. I will show recent results which were obtained due to cooperation between universities in Chambery, Versailles and Krakow.

Thursday 16th October 2008 at 10h15 Samuel Mimram (PPS, Paris 7),
Causalité dans les sémantiques interactives

Abstract: (Hide abstracts)
Les sémantiques de jeux ont été introduites pour capturer le comportement interactif des preuves en interprétant les formules par des jeux sur lesquels les preuves induisent des stratégies. L'une des difficultés majeures lors de la définition de telles sémantiques, est de les rendre précises, c'est-à-dire de caractériser les stratégies définissables, qui sont l'interprétation d'une preuve (ou d'un programme par la correspondance de Curry-Howard). L'extension des caractérisations habituelles à des langages de programmation comportant des constructions concurrentes nécessite de repenser en profondeur les définitions habituelles de sémantique des jeux, en menant une analyse fine de la structure dépendances entre les coups dans les stratégies. Nous présentons ici deux approches axiomatiques pour décrire cette structure : l'une externe, fondée sur la présence de certaines tuiles de permutation de coups dans les stratégies, l'autre interne, décrivant la catégorie des stratégies comme une structure algébrique libre.

Thursday 9th October 2008 at 10h Choco (LIX, LIP, IML, PPS),
Séminaire Choco

Abstract: (Hide abstracts)
Voir la page dédiée.

Thursday 2nd October 2008 at 10h15 Michaël Weiss (TCS-Sensor lab, Genève),
Calculabilité des pavages

Abstract: (Hide abstracts)
Au début des années 60, Wang a introduit un modèle de pavage du plan à l'aide de tuiles orientées de taille unitaire aux bords colorées pour résoudre des problèmes de logique. Ce modèle a été montré Turing-équivalent par Berger qui montra qu'un jeu de tuiles pouvait simuler une machine de Turing. Nous nous intéressons a la calculabilité de ce modèle en introduisant des outils sur les pavages permettant d'obtenir des résultats plus généraux sur les jeux de tuiles. A l'aide de notions de simulation, nous obtenons une première approche de l'universalité puis, nous montrons quelques uns des théorèmes fondamentaux de la calculabilité (Kleene, Rice...), dans le cadre des pavages, toujours relativement à certaines notions de simulation. Ces résultats nous permettront d'obtenir dans un premier temps de nouvelles preuves sur des théorèmes classiques des pavages et dans un deuxième temps de construire un cadre de construction de jeux de tuiles apériodiques.

Thursday 25th September 2008 at 10h15 Benoît Masson (LIF, Marseille),
Des piles de sable aux automates de sable

Abstract: (Hide abstracts)

Dans cet exposé, nous commencerons par résumer les résultats connus sur les modèles classiques de piles de sable (SPM, IPM(k)) et sur quelques-unes de leurs extensions. Nous verrons que l'approche combinatoire a des limites, justifiant ainsi leur étude au travers d'un nouveau système dynamique discret, les automates de sable.

Nous définirons ce système, en rappelant en permanence les liens existant entre celui-ci et un autre système dynamique mieux connu, les automates cellulaires. Puis, après avoir rappelé quelques-une des propriétés basiques des automates de sable, nous définirons des propriétés dynamiques à l'aide d'une topologie compacte inspirée de celle utilisée pour l'étude des automates cellulaires.

Ces propriétés permettent une étude plus globale de la dynamique d'un modèle donné, avec des techniques topologiques puissantes. Nous verrons ainsi comment classer les automates selon leur ``chaoticité'', en s'inspirant de la classification pour les automates cellulaires 1D de Kůrka. Ces résultats permettent de souligner que les automates de sable sont un système intermédiaire entre les automates cellulaires de dimension d et d+1.

Thursday 18th September 2008 at 10h15 Pierre Hyvernat (LAMA),
Fonctions booléennes et logique linéaire barycentrique

Abstract: (Hide abstracts)
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.

Thursday 11th September 2008 at 10h15 Guillaume Theyssier (LAMA),
Automates cellulaires, dynamique topologique et logique

Abstract: (Hide abstracts)
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.

Thursday 4th September 2008 at 10h15 Tom Hirschowitz (LAMA),
Vers des jeux topologiques

Abstract: (Hide abstracts)
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.

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.

Monday 1st September 2008 at 14h30 Clément Fumex (LAMA),
Container, dérivation de type et zipper, une répétition de soutenance

Abstract: (Hide abstracts)
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.

Thursday 3rd July 2008 at 10h15 Pierre Hyvernat (LAMA),
Les espaces cohérents et les espaces de finitude

Abstract: (Hide abstracts)
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 »...

Tuesday 1st July 2008 at 10h30 Laurent Fuchs (Université de Poitiers),
La droite réelle de Harthong-Reeb, un modèle d'une droite réelle constructive ?

Abstract: (Hide abstracts)
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 :

L'algèbre de Grassmann pour définir et manipuler des variétés linéaires discrètes et le plongement géométrique de structures topologiques combinatoires

Résumé :
L'algèbre de Grassmann fournit un langage de représentation des sous- espaces vectoriels d'un espace vectoriel. Ceci permet de manipuler ces sous-espaces sans faire référence directement à un système de coordonnées. Ceci est particulièrement utile lorsque la description ``analytique'' des sous-espaces est compliquée comme, par exemple, pour les variétés linéaires discrètes ou lorsque l'on veut pouvoir représenter la géométrie d'objets subdivisés en toutes dimension comme, par exemple, pour les cartes combinatoires généralisées.

Thursday 26th June 2008 at 10h15 Benoît Montagu (INRIA Rocquencourt),
A Logical Account of Type Generativity: Abstract types have open existential types

Abstract: (Hide abstracts)
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.

Thursday 19th June 2008 at 10h Choco (Southampton, Copenhague, et PPS),
Séminaire Choco: bigraphes

Abstract: (Hide abstracts)
Voir la page dédiée.

Tuesday 10th June 2008 at 10h15 Alexandre Miquel (PPS, Paris 7),
Réalisabilité

Abstract: (Hide abstracts)
Cours puis groupe de travail sur la réalisabilité avec Alexandre Miquel. Détails ici.

Thursday 29th May 2008 at 10h15 Fairouz Kamareddine (Université Heriot-Watt, Edimbourg),
Une computerisation graduelle des textes mathematiques dans le systeme MathLang

Abstract: (Hide abstracts)
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.

Thursday 22nd May 2008 at 10h15 Emmanuel Jeandel (LIF, Marseille),
Les pavages comme outils de la logique

Abstract: (Hide abstracts)
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.

Thursday 15th May 2008 at 10h15 Sylvain Lebresne (PPS, Paris 7 et Logical, LIX),
Un système d'exceptions pour le Système F

Abstract: (Hide abstracts)
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.

Thursday 24th April 2008 at 10h Projet Choco (PPS et Cambridge),
Quatrième journée Choco

Abstract: (Hide abstracts)
Cf le site idoine: http://choco.pps.jussieu.fr/events.

Thursday 17th April 2008 at 10h Samuel Thibault (XenSource),
Petite histoire des threads migrateurs et de l'algorithmie des bulles, ou comment les ambients sauvent la banquise

Abstract: (Hide abstracts)
Comme le montrent les publicités dans les magazines (multi-coeur par-ci, hyperthread par-là), la tendance des architectures des ordinateurs est à la parallélisation, et l'on commence donc dans le grand public à parler de programmation avec des threads. Du côté des machines de calcul scientifique, on mélange en fait allègrement ces technologies de manière hiérarchique pour aboutir à de véritables cathédrales, sur lesquelles on exécute une armée de threads. Cependant, pour obtenir une exécution _efficace_ (et donc économiser du temps, des machines ou de l'énergie), il est indispensable de distribuer de manière raisonnée ces threads sur ces machines. La tâche est d'autant plus ardue que les threads peuvent en créer d'autres, éventuellement de manière irrégulière. Durant ma thèse, j'ai proposé la notion de /bulles/, qui regroupent de manière récursive les threads et apportent ainsi une certaine structure aux applications de calcul scientifique. En modélisant par ailleurs les machines de calcul sous forme d'un arbre, on ramène ainsi notre problème à la mobilité des bulles et threads sur cet arbre. Une boîte à outil permet alors d'implémenter des algorithmes de placement/redistribution pour les appliquer à des applications bien concrètes. On peut alors observer des gains de performances de l'ordre de 20 à 40% par rapport à un ordonnancement classique ! Je débuterai mon exposé en expliquant quelques détails architecturaux importants par rapport à l'efficacité de l'exécution des threads d'une application. J'introduirai alors ce que j'entends par ``ordonnancement'', ``placement'' et ``migration'' des threads et bulles. Je présenterai ensuite la boîte à outils au travers de quelques exemples, et l'on pourra discuter notamment de la ressemblance intriguante avec des ambients.

Thursday 10th April 2008 at 10h15 Robert Bonnet (LAMA),
Algèbre libre sur un monoïde et demi-treillis compacts

Abstract: (Hide abstracts)
Cet exposé, est une partie d’un article en cours, en collaboration avec {\it Latifa Faouzi} (Fes et Casablanca) et se compose de deux parties indépendantes.
PARTIE I: $k$-algèbre libre sur un monoïde.
On considère un corps commutatif $k$ et un monoïde (= demi-groupe commutatif et unitaire) $M$. On désigne par $k[M]$ la $k$-algèbre sur le monoïde $M$, i.e. l’espace vectoriel sur $k$ ayant $M$ comme base, c’est alors aussi un anneau puisque $M$ est stable par produit. L’exemple type étant l’algèbre des polynômes sur $k$. Le corps $k$ étant fixé, on montre plusieurs propriétés de la classe des algèbres sur un monoïde. Par exemple $k[X] x k[Y]$ est une $k$-algèbre libre sur un monoïde. On développe aussi une classe plus large où le produit de deux élements de $M$ est soit $0$, soit un élement de $M$.
PARTIE II: Demi-treillis compact. Dans cette partie, les monoïdes ne sont pas unitaires. On considère un triplet $(L,O,.)$ où $(L,O)$ est un espace compact séparé, $(L,.)$ est un monoïde idempotent (mais sans unité). On suppose que l’application $(x,y) -> x. y$ est continue. En interprétant $x . y$ comme l’infimum de $x$ et de $y$, $(L,.)$ est un (inf-)demi-treillis et $.$ est continue. Noter que $L$ est alors un ensemble ordonné en posant $x \leq y$ ssi $x . y = x$. On montre quelques propriété de cette classe de structures. Par exemple, une telle structure possède un plus petit élément $0$ et toute partie non vide et filtrante supérieurement possède un supremum. La topologie est alors déterminée par l’ordre: une sous-base de la topologie est formée d’élements de la forme $U_x := \{ y \in L : y \geq x \}$ et $L \setminus U_x$ où $x$ est un élément “compact” de $L$. Ces notions de demi-treillis compacts apparaissent lors de l’étude des domaines et des treillis algébriques.
PARTIE III: Le lien. Si on considère le corps $k = \{0,1\}$ ayant deux éléments et le monoïde $M$ idempotent, alors $k[M]$ est une algèbre de Boole, dont l’espace des ultrafiltres (ou des idéaux maximaux) est un demi-treillis compact et “réciproquement”.
Bibliographie:
[1] Bourbaki N.: Eléments de mathématiques, Algèbre, Chapitres 1--3, Hermann, 1970.
[2] Lang S.: Algebra, Addision-Wiesley Pub, 1970.
[3] Gierz, G., Hofmann K. H., Keimel K., Lawson J. D., Mislove M. and Scott D. S.: Continuous lattices and domains, Encyclopedia of Mathematics and its Applications, 93. Cambridge University Press, Cambridge, 2003, 591 pp.

Tuesday 8th April 2008 at 10h30 Mouhammad Said (LAMA),
Géométrie multi-résolution des objets bruités

Abstract: (Hide abstracts)
L'objectif de cet exposé est de présenter le contexte et les motivations ayant conduit à mon sujet de thèse : Géométrie multirésolution des objets discrets bruités. On commencera par présenter quelques outils classiques autour des droites discrètes et leurs applications à l'estimation de quantités géométriques sur des formes discrètes. L'extension de ces outils aux formes discrètes bruitées sera ensuite abordée. On en déduira les quelques axes de recherche qui seront explorés dans ma thèse.

Thursday 3rd April 2008 at 10h15 Laurent Vuillon (LAMA),
Combinatoire des mots et conjecture de Fraenkel

Abstract: (Hide abstracts)
Ce séminaire donnera les liens entre un problème de recouvrement des entiers et la combinatoire des mots afin d'étudier la conjecture de Fraenkel. Cette conjecture a été formulée dans le cadre de la théorie des nombres il y a maintenant plus de 30 ans. Elle prétend que pour k > 2 entier fixé, il y a une unique façon de recouvrir les entiers par $k$ suites de Beatty avec des fréquences deux à deux distinctes. Ce problème peut être exprimé en termes de combinatoire des mots de la façon suivante: pour un alphabet à k lettres, il existe une unique suite équilibrée avec des fréquences de lettres deux à deux distinctes qui est exactement la suite de Fraenkel notée $(F r_k )^{omega}$ où F r_k = F r_{k-1} k F r_{k-1}, avec F r_3 = 1213121. Cette conjecture est prouvée pour k = 3, 4, 5, 6 d'après les travaux de Altman, Gaujal, Hordijk et Tijdeman ainsi que dans d'autres cas particuliers. Dans ce séminaire, nous présenterons donc une synthèse sur ce sujet et la résolution de la conjecture dans un cas particulier.

Tuesday 1st April 2008 at 10h30 Karim Nour (LAMA),
TBA

Abstract: (Hide abstracts)
TBA

Thursday 27th March 2008 at 10h15 Pierre Guillon (Univ. Marne-la-Vallée),
Automates cellulaires: trace et nilpotence

Abstract: (Hide abstracts)
Un automate cellulaire est un modèle de calcul parallèle synchrone, qui consiste en une juxtaposition d'automates d'état fini (cellules) dont l'état évolue dans le temps en fonction de celui de leurs voisins. Malgré la simplicité de cette règle locale, des comportements très variés peuvent être observés dans l'évolution d'une population de cellules.
Nous présentons ici quelques notions topologiques décrivant ces dynamiques. Nous nous intéressons en particulier à la nilpotence, qui correspond à un comportement ultimement stable. Nous en donnons une caractérisation utilisant la trace, qui est le mot infini représentant la suite des états pris par une cellule donnée.

Thursday 20th March 2008 at 10h Projet Choco (TBA),
Quatrième journée Choco

Abstract: (Hide abstracts)
Voir la page web idoine.

Thursday 13th March 2008 at 10h15 Lionel Vaux (IML),
λ-calcul algébrique

Abstract: (Hide abstracts)
On propose une extension naturelle du λ-calcul autorisant la formation de combinaisons linéaires de termes. Ceci reflète dans la syntaxe la sémantique quantitative du λ-calcul simplement typé dans les espaces de finitude, où les types sont interprétés par des espaces vectoriels particuliers, et les λ-termes par des fonctions entre ces espaces.
On étudie les effets de la présence de coefficients scalaires sur la réduction: après avoir étendu la β-réduction en une relation contextuelle et confluente, on s'intéresse à la cohérence du calcul et à des propriétés de normalisation dans un cadre typé.
On établit enfin une correspondance entre ce λ-calcul algébrique et le λ-calcul linéaire-algébrique d'Arrighi et Dowek en montrant qu'ils correspondent à deux stratégies de réduction (par nom et par valeur) d'une syntaxe commune.

Thursday 6th March 2008 at 10h15 Muhammad Humayoun (LAMA),
Software Specifications and Mathematical Proofs in Natural Languages

Abstract: (Hide abstracts)
Software specifications, Software/Hardware standards like RFCs, patents etc and Mathematical proofs are normally written in plain natural language. Natural languages are rich, complex, and ambiguous. Having this in mind, Formal methods try to solve this problem by replacing natural languages with rich mathematical formalisms which are understood by model checkers or theorem provers. They are very precise, accurate and clear but not easily understood by domain experts such as Software designers, programmers, engineers and Mathematicians.
This project is an attempt to make a connection between formal and natural languages. We are developing a controlled natural language having large coverage, which will be good enough for writing Software Specifications and Mathematical Proofs interactively.
We are currently working on parsing and translation of Mathematical proofs written in Natural language (English). Therefore I'll talk on Mathematical proofs for most of the time. Specifically I'll explain the implementation details.
Project homepage: http://www.lama.univ-savoie.fr/~humayoun/phd/index.html .

Friday 22nd February 2008 at 14h Damien Pous (Plume),
Soutenance de thèse

Abstract: (Hide abstracts)
TBA

Thursday 21st February 2008 at 10h Projet Choco (Bologne, INRIA Sophia et IML),
Troisième journée Choco

Abstract: (Hide abstracts)
Programme:

Thursday 14th February 2008 at 10h15 Giulio Manzonetto (PPS (Paris 7)),
Modèles effectifs du lambda calcul

Abstract: (Hide abstracts)
On étudie la question de l’existence d’un modèle non-syntaxique du lambda calcul appartenant aux sémantiques principales et ayant une théorie équationnelle ou inéquationnelle r.e. (récursivement énumérable).
Cette question est une généralisation naturelle du problème de Honsell et Ronchi Della Rocca (ouvert depuis plus que vingt ans) concernant l’existence d’un modèle continu de lambda-beta ou lambda-beta-eta. On introduit une notion adéquate de modèles effectifs du lambda-calcul, qui couvre en particulier tous les modèles qui ont été introduits individuellement en littérature, et on prouve que la théorie inéquationnelle d’un modèle effectif n’est jamais r.e.; en conséquence sa théorie équationnelle ne peut pas être lambda-beta ou lambda-beta-eta.
On montre aussi que la théorie équationnelle d’un modèle effectif vivant dans la sémantique stable ou fortement stable n’est jamais r.e. En ce qui concerne la sémantique continue de Scott, on démontre que la théorie inéquationnelle d’un modèle de graphe n’est jamais r.e. et qu’il existe beaucoup de modèles de graphes effectifs qui ont une théorie équationnelle qui n’est pas r.e.

Thursday 7th February 2008 at 10h15 Srecko Brlek (LaCIM, UQAM),
Ensembles discrets ronds

Abstract: (Hide abstracts)
We analyze the moment of inertia $\MI(S)$, relative to the center of gravity, of finite plane lattice sets $S$. We classify these sets according to their roundness: a set $S$ is rounder than a set $T$ if $\MI(S) < \MI(T)$. We show that roundest sets of a given size are strongly convex in the discrete sense. Moreover, we introduce the notion of quasi-discs and show that roundest sets are quasi-discs. We use weakly unimodal partitions and an inequality for the radius to make a table of roundest discrete sets up to size $40$. Surprisingly, it turns out that the radius of the smallest disc containing a roundest discrete set $S$ is not necessarily the radius of $S$ as a quasi-disc.

Thursday 31st January 2008 at 10h Projet Choco (PPS et IML),
Deuxième journée Choco

Abstract: (Hide abstracts)
Deuxième édition du séminaire Choco.
Le programme prévu est le suivant:
10h - 12h Damiano Mazza (PPS, Paris), Objets d'interaction et réseaux différentiels
14h - 15h30 Michele Pagani (PPS, Paris), Between interaction and semantics: visible acyclic nets
16h - 17h30 Lionel Vaux (IML, Marseille), Produit de convolution et composition parallèle

Thursday 24th January 2008 at 10h15 Tom Hirschowitz (LAMA),
Une théorie des théories des jeux

Abstract: (Hide abstracts)
(En collaboration avec André et Michel Hirschowitz.)
La sémantique des jeux a fait ses preuves comme source de modèles pleinement abstraits pour langages de programmation ou théories de la démonstration. De tels modèles apparaissent comme catégories de jeux et stratégies, mais on en compte de nombreuses variantes, qu'on ne sait pas bien relier entre elles. D'où la question: qu'est-ce qu'une catégorie de jeux et stratégies?
On donne une définition catégorique générale de jeu, en décrivant la catégorie de stratégies associée. On définit ensuite une construction catégorique générant un jeu à partir de données plus élémentaires. On montre comment les jeux de Hyland et Ong avec switching entrent dans ce cadre.

Thursday 17th January 2008 at 10h15 Francesco Zappa-Nardelli (Moscova (INRIA)),
Oracle Semantics for Concurrent Separation Logic

Abstract: (Hide abstracts)
We define (with machine-checked proofs in Coq) a modular operational semantics for Concurrent C minor---a language with shared memory, spawnable threads, and first-class locks. By modular we mean that one can reason about sequential control and data-flow knowing almost nothing about concurrency, and one can reason about concurrency knowing almost nothing about sequential control and data-flow constructs. We present a Concurrent Separation Logic with first-class locks and threads, and prove its soundness with respect to the operational semantics. Using our modularity principle, we proved the sequential CSL rules (those that are inherited from sequential Separation Logic) simply by adapting Appel & Blazy's machine-checked sequential-separation-logic soundness proofs with minimal changes. Our Concurrent C minor operational semantics is designed to connect to Leroy's optimizing (sequential) C minor compiler; we propose our modular semantics as a way to adapt Leroy's compiler-correctness proofs to the concurrent setting. Thus we will obtain end-to-end proofs: the properties you prove in Concurrent Separation Logic will be true of the program that actually executes on the machine. (Joint work with Aquinas Hobor and Andrew Appel (Princeton University)).

Wednesday 16th January 2008 at 14h Stéphane Le Roux (Mathematical Components (INRIA-Microsoft Research)),
Soutenance de thèse

Abstract: (Hide abstracts)
TBA

Thursday 10th January 2008 at 10h15 Frédéric Ruyer (LAMA),
Modèles pour le calcul et la logique

Abstract: (Hide abstracts)
Nous présentons une classe de modèles du lambda-calcul et de la logique du second ordre. Les modèles sont basés sur des treillis et interprètent la réduction, ainsi que la relation de réalisabilité, à l'aide de la relation d'ordre. Nous tenterons de dégager les liens avec les algèbres de Heyting et les modèles à base de cpo du lambda-calcul.

The seminar of the team LIMD is under the responsibility of Sebastien Tavenas.
Settings: See with increasing date . Hide abstracts
Other years: 2005, 2006, 2007, 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016, 2017, all years together.