ENS de Cachan
Département
Informatique
Visite du LIF et de l'IML









Navigation

En bref

  • Date: Jeudi 19 décembre 2013
  • Inscriptions: 37 étudiants
  • Départ : Jeudi 19 décembre, 6h19, Paris Gare de Lyon - Marseille 9h35
  • Retour: Jeudi 19 décembre, 20h06, Maseille - Paris Gare de Lyon 23h23
  • Accompagnateur: David Baelde
  • Coordinateur local: Pierre-Alain Reynier (LIF) et Emmanuel Beffara (IML)

Etudiants

L3 (22)

  • Bazin Théis, Begay Pierre-Léo, Comtat Félicien, Espitau Thomas, Gallot Paul,
  • Grange Julien, Guille-Escuret Charles, Hadjoudi Mounira, Hauseux Louis, Huguet Louis,
  • Jacomme Charlie, Jin Shendan, Karaboghossian Théo, Lanvin Victor, Lehaut Mathieu,
  • Ludmann Pierre, Marty Olivier, Rakotonirina Itsaka, Sablé-Meyer Mathias, Thiré François,
  • Winterhalter Théo, Yan Chen.

M1 et M2 (15)

  • Batmalle Hadrien, Beunardeau Marc, Fortin Marie, Hamel-de Le Court Edwin, Husson Adrien,
  • Journault Matthieu, Koutsos Adrien, Lallemand Joseph, Lick Anthony, Morgado Maxime,
  • Ohlmann Gaspard, Poulain Rémy, Randazzo Lucas, Razakarison Naina, Riesner Mélissa.

Les labos

Le LIF et l'IML sont réunis sur le site de Luminy de l'université Aix-Marseille.

Programme

Attention, programme en construction, à confirmer:

  • 11h00: Café d'accueil et présentation des labos
  • 11h30-12h15: Atelier 1
  • 12h15-13h00: Atelier 2
  • 13h00-14h30: Lunch
  • 14h30-15h15: Atelier 3
  • 15h15-16h00: Atelier 4
  • 16h00-16h15: Café
  • 16h15-17h00: Atelier 5

Groupe A (12)

  • Ateliers: Jeux, Combinatoire; Mobilite, Perceptron, CHAT
  • Étudiants: gallot lehaut thire bazin chen sjin winterhalter omarty karaboghossian huguet ??? ???

Groupe B (13)

  • Ateliers: Combinatoire, Langage; Realisabilite, Jeux, BioInfo
  • Étudiants: lanvin lallemand begay fortin poulain razakarison lick sable ludmal batmalle comtat grange guille

Groupe C (12)

  • Ateliers: Algebre, Security; CurryHoward, Flots, Mobilite
  • Étudiants: morgado koutsos husson rakotonirina espitau randazzo hamel jacomme hadjoudj journault ohlmann beunardeau

Ateliers

Liste des ateliers proposés, par mots-clés: Algèbre, Bioinfo, CHAT, Combinatoire, Curry-Howard, Flots, Jeux, Langage, Mobilité, Perceptron, Réalisabilité, Security.

[Curry-Howard] Emmanuel Beffara (en fait, Lionel Vaux) : Programmes, preuves et fonctions: le ménage à trois de Curry-Howard

Matériel en ligne: diapos et notes de cours.

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. Une lecture éclairée de telles sémantiques a permis l'introduction de systèmes de déduction jouissant à la fois de bonnes propriétés logiques et d'interprétations calculatoires fécondes. Cet exposé sera une introduction à cette correspondance, à partir de la logique minimale (lambda-calcul, déduction naturelle, interprétation de Brouwer-Heyting-Kolmogorov...) qui en illustre les idées fondatrices et permet d'esquisser les pistes de recherche acvtives du domaine.

[Security] Clara Bertolissi : Verification of security-aware workflow

Matériel en ligne: diapos, stage.

We are interested in security-aware workflow management systems, which are at the heart of several modern E-services. In this talk, we propose a new verification technique for ensuring the successful termination of workflows subject to authorization constraints. The methodology is based on state-of-the-art Satisfiability Modulo Theories techniques.

[Combinatoire] Anna Frid : Comptage de mots engendrés par morphismes et intervalles

Matériel en ligne: diapos.

Je vais donner une petite introduction à la combinatoire des mots et finir par poser des questions ouvertes dont l'étude peut impliquer des méthodes combinatoires, dynamiques et autres.

[Mobilité] Arnaud Labourel : Rendez-vous d'agents mobiles

Matériel en ligne: diapos, stage.

Les systèmes d'agents mobiles sont des environnements distribués dans lesquels les noeuds du réseau sont passifs et ce sont des agents mobiles qui s'occupent de l'exécution de l'algorithme. Le réseau est représenté par un graphe et les agents peuvent se déplacer d'un noeud a l'autre du graphe le long de ses arêtes. Les agents mobiles exécutent le même algorithme et sont autonomes. De plus, ils commencent tous sur des noeuds différents du graphe. Dans cet exposé, on va chercher à trouver des algorithmes permettant aux agents mobiles de tous se retrouver en un même noeud du graphe. Selon les hypothèses que l'on fait sur le graphe et les capacités des agents, ce problème connu sous le nom de problème de rendez-vous ne peut pas toujours être résolu. On donnera dans cet exposé des exemples de conditions nécessaires et/ou suffisantes afin que le rendez-vous soit réalisable.

[Algèbre] Glenn Merlet : Algèbre tropicale et réseaux

Certains problemes de synchronisation dans des reseaux sont lineaires par rapport aux operations dites «tropicales» max (vue comme addition) et plus (vue comme multiplication). On expliquera quelques questions et resultats lies a ce point de vue.

[Langage] Alexis Nasr : Nouvelles approches pour l'analyse syntaxique du langage naturel

Matériel en ligne: diapos et stage.

L'analyse syntaxique du langage naturel consiste a mettre au jour la structure syntaxique des énoncés. Il s'agit d'un domaine de recherche qui a pris son essor avec les travaux de Noam Chomsky en linguistique formelle dans les années cinquante. Dans l'approche traditionnelle, les grammaires, qui constituent le coeur des analyseurs syntaxiques étaient mises au point par des linguistes. L'avènement de corpus syntaxiquement annotés (des collections de phrases dont la structure syntaxique est représentée explicitement) a été à l'orginine de nouvelles approches pour de l'analyse syntaxique dans lesquelles les grammaires sont apprises directement à partir des données. On décrira dans cet exposé des modèles récents d'analyseurs syntaxiques, on montrera leurs limites et on proposera des méthodes d'y remédier en utilisant notamment des données extraites de très grosses collections de données.

[Flots] Guyslain Naves : Une petite plongée dans les flots

Les flots sont un outil théorique pour étudier des problèmes de transport : comment transporter un maximum de biens ou personnes entre différents lieux, à un coût minimal ? Les plongements de métriques consistent à placer des points dans un espace métrique (par exemple le plan Euclidien), de sorte que chaque paire de points respecte une contrainte de distance relative. Ces deux objets, apparemment sans lien, possèdent en fait une relation de dualité : tout énoncé sur les flots donne lieu à un énoncé équivalent pour les plongements de métriques. Le but de cet exposé sera d'expliquer cette dualité et d'en voir quelques conséquences, notamment algorithmique.

[CHAT] Peter Niebert : Visite guidée de l'exposition LED's CHAT

En fin de journée nous vous proposons une visite guidée de l'installation LED's CHAT dans la Maison de la Région à 5min de la Gare Saint-Charles. Une page web un peu publicitaire sur cette exposition se trouve ici : http://leds-chat.net. L'intérêt pour vous est un modèle de programmation un peu particulier que nous avons inventé et nommé la programmation cellulaire. Il s'agit d'un mélange de programmation synchrone et d'algorithmique distribuée avec comme source d'inspiration aussi les automates cellulaires. Cette forme de programmation (caractérisée space par un de nos étudiants) trouve son expression ludique dans des jeux de lumière exposés. Sur le plan théorique, nous vous expliquerons le modèle de programmation avec quelques exemples. Toutefois, il s'agira d'un exposé bien décontracté… Si vous êtes intéressés, on vous rendra accessible l'environnement intégré de développement et de simulations pour faire vos propres expériences.

[Perceptron] Liva Ralaivola : Le Perceptron en peu de bits

Une problématique phare de l'apprentissage automatique est celle de la classification : à partir d'un ensemble d'observations étiquetées S = {(x_n , y_n)}_n=1..N où x_n ∈ X et y_n ∈ {-1, +1}, l'objectif est de construire un classifieur f ∈ {-1, +1}^X capable de prédire adéquatement - on parle de généralisation - la classe associée à des observations x non présentes dans S. L'algorithme du Perceptron (Rosenblatt, 58) est un algorithme très simple et très efficace de classification linéaire, dont les propriétés théoriques de convergence et de généralisation expliquent sa popularité. Cependant, l'analyse théorique du Perceptron repose uniquement sur des arguments d'algèbre linéaire et ne prend nullement en compte la vocation de l'algorithme à être implanté en machine, où le nombre de bits disponibles, notamment pour la représentation des réels, est forcément limité. Une problématique qui se pose ainsi, et qui prend particulièrement son sens face à la multiplication de dispositifs de calcul portables, est celle de savoir quelles sont les propriétés (convergence, généralisation) du Perceptron sur une architecture à B bits. Cette problématique ouvre plus généralement la question d'une nouvelle manière d'appréhender l'apprentissage automatique, qui se ferait avec une sensibilité plus grande à des contraintes informatiques.

F. Rosenblatt (1958), "The perceptron : a probabilistic model for information storage and organization in the brain".

[Réalisabilité] Laurent Regnier : Que signifie « que signifie l'axiome du choix ? » ?

Traditionnellement la logique s'occupe de vérité : quand peut-on dire qu'un énoncé est vrai ? Il se trouve que lorsque l'on se restreint aux énoncés mathématiques, on peut formuler cette question complètement mathématiquement; en particulier on peut définir l'interprétation d'une formule dans une structure, essentiellement l'ensemble des objets sur lesquels la formule est vraie. Ceci donne une notion relativement vide de la vérité: la vérité est... ce qui est vrai.

À partir des années 50 un nouveau champ d'investigation s'ouvre à la logique; l'appareillage technique développé jusqu'alors peut également s'appliquer à la question : qu'est-ce qu'une démonstration ? Une réponse a cette question est fournie par la correspondance preuve/programme qui repose sur la définition, dans des systèmes logiques appropriés, d'un calcul sur les démonstrations (élimination des coupures, normalisation) permettant de voir celles-ci comme des programmes. Les formules deviennent alors des spécifications de programmes: un programme de type A est une démonstration (sans coupure) de A. Ceci donne un sens aux formules très différent de leur sens mathématique: par exemple la tautologie (A → A) → (A → A) qui n'a aucun sens mathématique (elle est juste vraie) est essentiellement la spécification d'une boucle for.

On définit ainsi une sémantique des formules beaucoup plus riche que la sémantique usuelle, tellement riche que l'on est un peu perdu; dans le cas de formules très simples comme celle ci-dessus on peut facilement trouver leur interprétation en tant que type, mais qu'arrive-t-il lorsque l'on s'attaque à des formules dotées d'un réel sens mathématique? Que fait un programme qui réaliserait la spécification énoncée par l'axiome du choix? (Ce type de question a motivé l'élaboration par Jean-Louis Krivine d'une théorie aujourd'hui connue sous le nom de "réalisabilité classique").

[Jeux] Luigi Santocanale : Des jeux de parité aux cercles vertueux dans les preuves

Matériel en ligne: diapos et stage.

Dans cet exposé je présenterai la notion de jeu de parité et ses liens avec la logique. Si un tel jeu ne contient pas des circuits, on peut le considérer comme une formule logique ; une stratégie gagnante pour un des deux joueurs pourra alors s'interpréter comme un preuve de cette formule. Que se passe-t-il si le jeu contient des circuits ? Nous verrons qu'on peut interpréter un tel jeu aussi comme un formule logique, grâce aux notions de plus petit et plus grand points fixes d'une fonction monotone. Une stratégie gagnante s'interprétera alors comme une preuve, mais d'une nature très particulière car elle contiendra aussi des circuits. Faut il considérer ces circuits comme des cercles vicieux ou vertueux ? Un peu d'algèbre pour les points fixes nous explique que c'est bien le dernier cas.

[Bioinfo] Sylvain Sené : Automata networks as models of regulation netwoks : a return to basics

Computer science and biology have been intimately related since the 1940's through the term of model (computational model on one side and "modelling model" on the other). Historically, the first and basic model that took a key place in both these two disciplines was that of automata networks, and more precisely of Boolean automata networks (BANs). The reason for that comes from the simplicity of their setting, their high level of abstraction that gives them important representational capacities and their ability to capture relevantly most of the basic but essential intricacies and heterogeneities of real-life systems. This presentation will deliver the point of view of a theoretical computer sciencist and bio-informatician on computer science and biology interconnections, mainly in the context of genetic regulations. It will do so by giving an overview of BANs and explaining why their study is worthwhile for going further in the understanding of general laws that govern living systems.

Propositions de stages

Vous trouverez ci-dessous quelques sujets de stage possibles. Il ne s'agit pas des seules possibilités et vous êtes encouragés à contacter tout orateur dont le sujet vous intéresserait.

  • Stage L3 avec Clara Bertolissi, Symbolic verification of workflows with security constraints (fiche)
  • Stage L3 avec Arnaud Labourel, Amélioration des algorithmes de robots mobiles par l'utilisation de la géolocalisation (fiche)
  • Stage L3 avec Alexis Nasr, Intégration de connaissances sémantiques et syntaxique de "haut niveau" dans un analyseur syntaxique (fiche)
  • Stage L3 avec Luigi Santocanale, Preuves circulaires pour la logique linéaire et sémantique des revêtements (fiche)


Contacter le Département Informatique
Dernières modifications : le 26/01/2014