ENS de Cachan
Département
Informatique
Marseille Visit









Date
Thursday, November 23, 2017
Participants
42 students
Departure
November 23, 2017, 06:07 from Gare de Lyon (arrival in Marseille St Charles at 09:41). We meet at 05:50 at the train station at the entrance of the train's platform. For those living near the campus, this means taking the 5:05 RER B train in Bagneux.
Return
November 23, 2017, 22:23 in Gare de Lyon (departure from Marseille St Charles at 19:06)
Overseer
Sylvain Schmitz
Local organiser
Benjamin Monmege

Visited Labs

We will be welcomed at the library at 11am; here is the planned itinerary:

Program of the Day

See the schedule with the students' repartition into groups.

Alexandra Bac (LSIS, G-MOD): Modélisation géométrique : à la croisée des chemins entre informatique et mathématiques
Au cours de cet exposé, nous brosserons les grandes lignes de la recherche en Modélisation géométrique, et en particulier, des travaux menés dans l'équipe G-Mod du laboratoire LSIS. La modélisation géométrique est au cœur de l'informatique graphique et en même temps recouvre différents domaines des Mathématiques (variétés différentielles pour les aspects d'étude des surfaces, optimisation non linéaire, analyse numérique, topologie, topologie algébrique). Nous aborderons quelques exemples de travaux orientés tant vers des buts fondamentaux qu'appliqués. En particulier, nous ferons un petit détour par l'homologie algorithmique et ses liens avec la géométrie.
Jérémie Chalopin (LIF, DALGO): Jouer au gendarme et au voleur pour approximer l'hyperbolicité
Dans le jeu du gendarme et du voleur, deux joueurs (le gendarme et le voleur) évoluent sur les sommets d'un graphe en se déplaçant chacun leur tour. Le but du gendarme est d'attraper le voleur (en étant sur le même sommet que lui); le but du voleur est de réussir à s'échapper perpétuellement. Dans cet exposé, on considère une variante du jeu du gendarme et et du voleur où les joueurs ont des vitesses différentes: à chaque étape, le gendarme peut se déplacer le long d'un chemin de longueur au plus s' et le voleur le long d'un chemin de longueur au plus s (tout en évitant la position du gendarme). Un graphe est (s,s')-gagnant si un gendarme avec une vitesse s' a une stratégie pour capturer n'importe quel voleur se déplaçant à vitesse s. Les graphes delta-hyperboliques sont des graphes qui ressemblent à des arbres d'un point de vue métrique. On présentera quelques unes des nombreuses définitions de l'hyperbolicité. On présentera ensuite nos résultats reliant le jeu du gendarme et du voleur et l'hyperbolicité du graphe. On montre que si un graphe est delta-hyperbolique, alors il est (2r,r+2delta)-gagnant pour tout r. Réciproquement, on montre que si un graphe est (s,s')-gagnant (avec s > s'), alors il est O(s^2)-hyperbolique.
Basile Couëtoux (LIF, ACRO): Inapproximabilité d'un problème de chemin coloré
Étant donné un graphe dirigé acyclique dont les sommets sont colorés, on cherche un chemin qui collecte un nombre maximum de couleurs. C'est un problème d'optimisation combinatoire qui est NP-difficile, ainsi cela justifie de rechercher une solution approchée. On montrera que ce problème est difficile à approximer dans un premier temps, et ensuite grâce à un argument diagonal qu'il n'est pas possible de l'approximer avec un rapport constant.
Anna E. Frid (I2M, GDAC): Mots de Fibonacci, mots sturmiens et systèmes de numération d'Ostrowski
Dans le système de numération de Fibonacci, tout nombre n est exprimé comme une somme de nombres de Fibonacci définis par F_0=1, F_1=2, F_k=F_{k-1}+F_{k-2} pour tout k>1. Par exemple, 14=13+1=F_5+F_0, donc 14 a comme représentation la suite 100001, ou bien 11001, car 14=8+5+1. Nous considérons le lien entre une généralisation de ce système qui s'appelle le système de numération d'Ostrowski et la description des palindromes dans les mots sturmiens qui, à leur tour, généralisent le mot de Fibonacci abaababaabaababaab... construit par la récurrence s_{-1}=b, s_0=a, s_n=s_{n-1}s_{n-2} pour tout n>0. En particulier, s_1=ab, s_2=aba et s_5=abaababaabaab. Nous voyons que la longueur de s_n est F_n pour tout n. Je vais présenter quelques résultats et plusieurs problèmes ouverts sur ce lien.
Emmanuel Godard and Damien Imbs (LIF, DALGO): Calculabilité distribuée et topologie discrète
Un système distribué doit fonctionner correctement même en cas de défaillances d'une partie du système. Nous présenterons des tâches distribuées fondamentales et montreront que dans certains cas celles-ci n'ont pas de solution algorithmique. Les preuves de ces impossibilités peuvent être généralisées par des techniques de topologie discrète. Nous évoquerons pour finir un résultat de topologie des années 30 qui a été utilisé par les lauréats du prix Gödel 2004 pour leurs théorèmes de calculabilité distribuée.
Charles Grellois (LSIS, LIRICA): Vérification des programmes d'ordre supérieur
La vérification des programmes fonctionnels fait intervenir le concept d'ordre supérieur : une fonction peut prendre en argument une fonction. Par exemple, la fonction "map" prend en argument une liste d'entiers et une fonction des entiers vers les entiers ; elle applique la fonction à chaque élément de la liste, et renvoie le résultat. On peut modéliser de tels programmes à l'aide de schémas de récursion d'ordre supérieur, ou d'un lambda-calcul avec points fixes. Dans les deux cas, qui sont équivalents, ces modélisations permettent d'obtenir des représentations finies d'un arbre infini, représentant les comportements possibles du programme à analyser. On s'intéresse alors à la vérification de propriétés sur cet arbre infini de comportements, vérification que l'on veut effectuer directement sur la représentation finie sous forme de schéma de récursion (ou de lambda-terme récursif), afin d'espérer des résultats de décidabilité. Il s'avère qu'on peut vérifier les formules de MSO, une logique standard en vérification, sur ces arbres infinis : il existe une procédure de décision qui, étant donné un schéma de récursion représentant finiment un arbre infini, et une formule MSO, calcule si l'arbre infini satisfait la formule. Ce résultat, prouvé en 2006 par Ong en utilisant la sémantique des jeux, a reçu beaucoup d'attention et a été prouvé de nouveau plusieurs fois depuis, en utilisant de la sémantique, de la théorie des types, ou des automates à piles de piles de piles... Au cours de cet atelier, j'expliquerai les bases : comment les schémas de récursion représentent les comportements de programmes fonctionnels, comment des automates permettent de vérifier MSO dessus, quels problèmes on considère, et je donnerai une rapide intuition de la connexion avec la théorie des types et la sémantique de la logique linéaire. Mon but sera de montrer que la vérification d'ordre supérieur se situe à la croisée de plusieurs belles directions de recherche de l'informatique théorique actuelle : théorie des automates, théorie des types, sémantique, logique (linéaire)...
Pierre Guillon (I2M, GDAC): Automates cellulaires
Les automates cellulaires, modèles de systèmes complexes, sont à la fois étudiés comme des systèmes dynamiques et comme des modèles de calcul ; on fera un panorama de différentes propriétés qui exhibent des liens avec la dynamique topologique, la théorie des automates, la logique, la théorie de la mesure...
Hachem Kadri and Giuseppe Di Molfetta (LIF, QARMA and CANA): Quantum Machine Learning
Cet atelier vise à donner une vue d'ensemble du domaine de l'apprentissage quantique. Après une introduction générale des domaines "Quantum Computing" et "Machine Learning", cet atelier aura comme but de situer l'intérêt et les enjeux d'une imbrication étroite des deux domaines. Des travaux récents ainsi que des pistes de recherche à la frontière des deux domaines seront présentés.
Kolja Knauer (LIF, ACRO): Manger du chocolat, des posets et des graphes
CHOMP est un jeux à deux joueurs qui partagent une tablette de chocolat avec un carré empoisonné. Le joueur qui mange ce carré a perdu. Le genre de questions, qu'on se pose c'est : Quel joueur a une stratégie gagnante ? Est-ce qu'on peut donner une stratégie explicite ? Ce jeu peut être généralisé aux posets et aux graphes. Nous regarderons plusieurs familles où on sait quel joueur a une stratégie gagnante.
Julien Lefèvre (LSIS, I&M): Neuro-anatomie computationnelle
L'anatomie computationnelle est un champ de recherche jeune mais porteur, au croisement de l'informatique, des mathématiques appliquées, de la médecine et de la biologie. Il consiste en la modélisation de formes biologiques, pour réaliser des analyses statistiques à visées prédictives (diagnostic de pathologies) ou encore pour simuler des dynamiques spatiotemporelles proprement biologiques (croissance de tumeur, morphogénèse du cortex cérébral). Nous présenterons quelques thématiques issues de la neuroimagerie et montrerons en quoi elles donnent lieu à des questions théoriques à part entière qui concernent le machine learning ou encore l'analyse spectrale des surfaces.
Alexis Nasr (LIF, TALEP): Traitement automatique des langues
Cet atelier proposera une introduction au domaine du traitement automatique des langues (TAL). Nous décrirons quelques tâches du TAL ainsi que des modèles qui permettent de les traiter. L'accent sera mis sur les méthodes numériques, issues de l'apprentissage automatique, ainsi que sur les problèmes algorithmiques qui découlent de leur mise en oeuvre. Après cette introduction, on parlera de réseaux de neurones profonds qui se sont beaucoup développés ces dernières années. On verra comment, à travers l'apprentissage de représentation, ils proposent des représentations vectorielles continues d'entités symboliques.
Pierre-Alain Reynier (LIF, MOVE): Déterminisation de transducteurs
La notion de déterminisme est essentielle pour obtenir par exemple une évaluation efficace d'un modèle de calcul. Il est bien connu qu'il est toujours possible de déterminiser les automates finis. Lorsque l'on considère les transducteurs, qui sont obtenus en associant aux transitions des mots produits en sortie, ce résultat n'est plus valable. En effet, il est facile de voir (exercice !) que les transducteurs non déterministes sont strictement plus expressifs que les transducteurs déterministes. Nous commencerons dans cet exposé par présenter une caractérisation des transducteurs qui peuvent être déterminisés, obtenue par Choffrut en 1977. Nous présenterons ensuite des extensions récentes de ce résultat, qui permettent par exemple de réécrire un transducteur non-déterministe comme une union finie de transducteurs déterministes. Nous conclurons en présentant les travaux actuels en lien avec cette question.
Sylvain Sené and Kévin Perrot (LIF, CANA): à la découverte du calcul naturel
Après une rapide présentation du domaine du calcul naturel, nous vous proposons de découvrir certains thèmes de l'équipe CANA à travers deux présentations courtes : - La première traitera des réseaux d'automates, un type de systèmes dynamiques discrets particulièrement pertinent pour appréhender des propriétés de convergence dynamique, de complexité et de calculabilité mais aussi pour modéliser des systèmes réels, tels que les réseaux biologiques. L'idée est ici de donner un panorama des grandes questions théoriques se posant actuellement sur ces objets mathématiques. - La seconde traitera des piles de sable, une sous-famille des automates cellulaires, dont les règles d'évolution locales sont "simples", mais dont le comportement est particulièrement "complexe" à analyser. En jouant avec un simulateur nous observerons que les interactions microscopiques entre les grains produisent des motifs macroscopiques qu'il nous est facile d'exhiber, mais difficile d'expliquer pour des raisons fondamentales qui seront discutées.
Laurent Tichit (I2M, MEB): Biologie des systèmes et des réseaux
Nous nous intéressons aux réseaux de régulation génétiques et aux réseaux d'interaction biologique à grande échelle. La présentation va s'articuler autour de deux grands axes : d'une part le développement de méthodes de calcul pour l'analyse de grands réseaux biologiques et d'autre part des outils de mathématiques discrètes pour la modélisation de réseaux de régulation.
Lionel Vaux (I2M, LDP): Programmes, preuves et fonctions : le ménage à trois de Curry-Howard
La correspondance de Curry-Howard promeut le point de vue selon lequel démonstrations et programmes sont des objets de même nature, l'élimination des coupures étant le pendant logique de l'exécution. L'étude des invariants des processus de calcul est le but des sémantiques dénotationnelles : en interprétant les types (formules logiques) comme des espaces structurés et les programmes (démonstrations) comme des morphismes entre ces espaces, elles capturent des propriétés essentielles du calcul. L'exposé introduira cette correspondance dans le cas le mieux connu: la logique implicative minimale = le λ-calcul simplement typé. On esquissera comment une lecture sémantique de cette correspondance a permis l'invention de la logique linéaire.


Contacter le Département Informatique
Dernières modifications : le 22/11/2017