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.