Preuves, Programmes et Systèmes

Groupe de repos

À venir

Déjà passés

2011

• Lundi 5 décembre, 10h - 16h, salle 5D91 (Chevaleret)
  
  Jean Krivine, Russ Harmer
  Formal Cellular Machinery: term rewriting and biological modeling
  Compléments de l'exposé de Trouville et développement sur le domaine général

2009

• Jeudi 16 décembre, 14h - 16h, Chloé Azencott, **Statistical Machine Learning and Data Mining for Chemoinformatics and Drug Discovery**
  I will give a short overview of the modern drug discovery process, identifying the benefits that computational approaches can bring to the field in terms of rationalization, costs, and time necessary to bring a new drug to the market, and examime some open questions in chemoinformatics. In particular, I will address the issue of the representation of small molecular compounds, discuss how to perform fast and accurate virtual screening, and (if time permits) give some insights on how to approach the prediction of chemical reactions.
  Gâteaux : Thibaut, Marie-Aude, peut-être d'autres...

• vendredi 9 octobre, 16h - 18h, Danko Ilik, **Modèles de Kripke et normalisation-par-évaluation en lambda-calcul**. (slides et handout)
  An evaluator for simply typed lambda calculus (STLC) can be given explicitly by giving a rewrite system that specifies beta-reduction, but it can also be given implicitly by interpreting STLC in a suitable meta-language, a technique known as normalisation-by-evaluation. The interpretation is done by a Kripke model, that we will look at in detail. The notion of model can be refined so that it allows normalisation-by-evaluation for computational _classical_ logic as well (STLC+call/cc).
  Gâteau: Jonas, une recette de grand-mère...

• vendredi 15 mai, 14h-16h, (6A92) Pierre Letouzey, le point sur coq, n'oubliez pas votre machine.
  Coq au vin, Stéphane

• mercredi 8 avril, 16h-17h, (6A92) Stéphane Zimmermann, introduction à la ludique (3).
  Gâteau: Samuel

• mercredi 1 avril (6A92), 16h-17h, Stéphane Zimmermann, introduction à la ludique (2).
  Les intuitions provenant du calcul des séquents ayant été vues, on posera les définitions formelles d'actions, chroniques et desseins pour eux-même. Le reste de la séance sera dédié à l'interaction entre desseins via les réseaux de coupure. Cette dynamique du calcul sera vue sous deux angles : tout d'abord voir l'interaction à l'aide d'une machine abstraite pour mettre en avant le côté "mécanique" de la réduction, puis voir cette interaction comme quotient d'ordres topologiques pour en avoir une vision plus directement mathématique.
  On terminera par indiquer les théorèmes analytiques sur cette interaction, qui indiquent que celle-ci se comporte de manière raisonnable.
  Le gâteau sera réalisé par l'orateur recette.

• mardi 24 mars, 16h-17h, 0D1 Stéphane Zimmermann, introduction à la ludique (1).
  La ludique est une théorie du calcul fondée sur l'interaction entre des objets particuliers, les desseins. Dans la première partie de cette introduction, on partira de la logique linéaire multiplicative additive, puis on visitera la polarisation et la focalisation pour gagner des connecteurs synthétiques. A partir de là, on introduira un peu de locativité et on s'abstraira des séquents pour obtenir ces fameux desseins.
  Le cuisinier Fabien anciennement élu nous a régalé avec son Crumble.

• vendredi 6 mars, 10h-12h, 6A92 : Juliusz Chroboczek, protocole réseaux et Babel 2.
  Je vous montrerai un raffinement de vecteur de distance naïf, le vecteur de distance sans boucles, collégial et démocratique. Après avoir rapidement montré comment ce genre de techniques est aujourd'hui utilisé sur l'Internet Global par le protocole BGP, et dit quelques mots sur le protocole interne « EIGRP » de Cisco, je vous montrerai comment les techniques sans boucles peuvent être utilisées pour construire un protocole de routage unitaire utilisable en pratique dans les réseaux maillés sans fil – qu'on pourrait par exemple appeler Babel.
  Le cuisinier sera Fabien, élu haut-la-main à 9 voix sur 13 et remplacé à la volée par Thibaut recette

• vendredi 20 fév., 14h-16h, 6A92 : Juliusz Chroboczek, protocole réseaux et Babel 1.
  Je mettrai en place la problématique du routage « next-hop » et passerai rapidement en revue les techniques existantes, la technique par vecteur de distance et la technique par état de lien. Je mettrai aussi en évidence les limitations du vecteur de distance classique.
  En guise de goûter, gâteau par Gabriel. recette

2008

• mercredi 10 déc., 11h-12h, 6A92 : Yann Régis-Gianas, GADTs (Types Algébriques Généralisés), deuxième partie. transparents
  Au menu du petit déjeuner, gâteau au pommes par Nathalia. recette

• jeudi 27 nov., 10h-11h : Thibaut Balabonski, les clefs pour comprendre l'analyse statique de systèmes parallèles
  par des méthodes géométriques. transparents

• mercredi 26 nov., 16h-18h, 6A92 : Yann Régis-Gianas, GADTs (Types Algébriques Généralisés). transparents
  Ce rendez-vous sera accompagné par un délicieux /vlaai limbourgeois/ réalisés par Jaap. recette

• vendredi 20 juin, 14h, 6A92 : Emmanuel Haucourt, Le pointeur d'instruction d'un programme parallèle se déplace sur une surface dirigée de dimension supérieure.
  Après avoir rapidement décrit un langage jouet, je préciserai le sens du titre de l'exposé. L'intervention des surfaces de dimension supérieures conduit naturellement à l'emploi de méthodes issues de la topologie algébrique. L'idée étant de trouver des invariants de la surface dirigée qui caractérise en partie le programme parallèle que l'on souhaite analyser. Durant l'exposé, quelques notions mathématiques feront un passage
  - Les espaces partiellement ordonnés.
  - Le foncteur "catégorie fondamentale".
  Et si le temps le permet
  - La construction de la catégorie des composantes.
  - La liberté du monoïde (muni du produit cartésien) des classes d'isomorphisme de catégories finies sans boucle et connexes. (objet du stage de Thibaut Balabonski). Le tout servi avec beaucoup d'exemples.

• jeudi 10 avril, 13h30-16h : Olivier Danvy, Un vademecuum pour les continuations. article1 article2

• mardi 25 mars, 14h : Alain Riazuelo, Voyage autour (et à l'intérieur) d'un trou noir
  À quoi ressemblent les distorsions gravitationnelles au voisinage immédiat d'un trou noir ? Quelle est la dernière image qu'il soit donné de voir à un observateur atteignant une singularité ? Le passage de l'horizon d'un trou noir se traduit-il par un effet observable ? À quoi ressemblent un trou blanc, une singularité nue ou le passage par un trou de ver ? Si la structure géométrique d'un espace-temps contenant un trou noir a été abondamment étudiée et que leurs géodésiques ont été classifiées depuis longtemps, relativement peu de travaux se sont focalisés sur la traduction visuelle de toute la panoplie des effets relativistes produits par les trous noirs, alors que les moyens informatiques modernes les rendent relativement aisés à simuler. Dans ce séminaire à vocation pédagogique, je présenterai quelques résultats

obtenus récemment sur ce sujet, avec de nombreuses illustrations sous la forme d'animations dont l'objectif est d'allier réalisme du point de vue scientifique à un certain souci esthétique. transparents

• mercredi 19 mars et jeudi 20, 14h : Alexandre Miquel, Les témoins en réalisabilité classique. transparents

• mercredi 6 février et lundi 11, 14h : Yves LegrandGérard, Formules valides, jeux et protocole réseaux
  résumé dans son article avec Jean-Louis Krivine, article.
• mercredi 23 janvier, 14h, 6A92 : Olivier Laurent, Une introduction à la géométrie de l'interaction.

2007

• mercredi 12 décembre, 13h30, 6A92 : Sylvain Pradalier, Modélisation de systèmes chimiques.
  Dans la modelisation des systemes chimiques, la dynamique peut etre regie par deux paradigmes distincts. Le modele continu base sur des equations differentielles obeit a la loi d'action de masse. Le modele discret base sur une simulation stochastique des differents comportements possibles est gouvernee par l'algorithme de Gillespie. On represente ces modeles utilises par les chimistes par un systeme de reecriture. Une algebre de processus, proche de CCS, est introduite, pour laquelle des sémantiques continue et discretes sont definies. Deux codages sont ensuite presentes, de l'algebre de processus vers le systeme de reecriture et vice-versa. Ces deux codages preservent les deux sémantiques, continue et discrète.

• mercredi 21 novembre, 14h, 6A92 : Jérôme Vouillon, Monades pour la programmation impérative.