Programme de l’UE :
- Preuve interactive
Système Coq
Types dépendants
Polymorphisme
Arithmétique - Preuve automatique
Calcul des séquents
Résolution
Théories décidables
Lien vers la page www du cours.
Intervenants
- Colin Riba, MdC ENS Lyon
- ..
Lien vers la page www du cours.
What computing resources do we need to solve a computational problem? The computational complexity theory studies this question from a structural point of view. Building up on the Turing machine model, we will discover and study deterministic and nondeterministic complexity classes, space and time complexity and hierarchy, completeness, randomized algorithms classes, boolean circuits and counting classes.
Bibliography:
Computational Complexity: A Modern Approach, Sanjeev Arora and Boaz Barak (mostly chapters 1 to 7)
more about computational complexity
De quelles ressources avons nous besoins pour résoudre un problème, faire un calcul ? La théorie de la complexité algorithmique étudie ce problème d’un point de vue structurel. En nous appuyant sur le modèle des machines de Turing, nous étudierons les classes de complexité déterministes et non déterministes, en temps et en espace, les hiérarchies entre ces classes, les problèmes complets, les algorithmes et classes probabilistes, les classes définies par les circuits ainsi que quelques notions sur les classes de comptage.
Bibliographie :
Computational Complexity: A Modern Approach, Sanjeev Arora and Boaz Barak, principalement les chapitres 1 à 7
Pour en savoir plus sur la théorie de la complexité algorithmique
https://fr.wikipedia.org/wiki/Théorie_de_la_complexité_(informatique_théorique)
Page du cours (for 2013-2014)
L’arithmétique des ordinateurs s’intéresse à la fois à la conception d’opérateurs arithmétiques, et à leur utilisation fine pour réaliser des fonctions plus complexes.
Ce cours présente un panorama des représentations utilisées en machine pour manipuler les nombres entiers, les réels et les polynômes, ainsi que l’algorithmique associée à chaque représentation pour réaliser les opérations de base (addition, multiplication, division, racine carrée… ) et calculer des fonctions « élémentaires » (logarithme, exponentielle, fonctions trigonométriques, etc.).
On s’intéressera d’abord à la manipulation de nombres en « précision fixée » (entiers, virgule flottante, norme IEEE 754) ainsi qu’à diverses techniques permettant d’augmenter ou de garantir la précision des calculs: on montrera ainsi qu’une arithmétique « approchée » comme la virgule flottante permet de faire des calculs exacts.
On étudiera ensuite la complexité et l’algorithmique des opérations de base sur les polynômes (multiplication, division, évaluation, interpolation), en arithmétique exacte.
Enfin, nous aborderons la question du calcul sur les polynômes en arithmétique approchée. Cela permettra d’une part de présenter les notions fondamentales de conditionnement d’un problème et de stabilité d’un algorithme et, d’autre part, de comprendre pourquoi l’évaluation polynomiale est de plus en plus souvent au coeur des implantations (logicielles ou matérielles) d’opérateurs arithmétiques de base comme la division ou la racine carrée.
Le parallélisme est devenu incontournable en informatique, le moindre processeur étant multi-cœurs. Cette UE a pour objet la conception d’algorithmes parallèles efficaces et leur mise en œuvre pratique.
Les séances de cours auront pour objet les modèles théoriques utilisés pour la conception et l’analyse des algorithmes et l’étude de problèmes algorithmiques particuliers (complexité, définition et analyse d’algorithmes, algorithmes d’approximations, etc.).
Les séances de cours seront accompagnées de six séances de TDs et de six séances de TPs. Les TPs auront pour but l’initiation à la programmation parallèle par passage de messages (MPI).
Plan indicatif des cours:
– Modèle théorique des réseaux de tri
– Modèle théorique des PRAMs
– Algorithmique sur anneau et grille de processeurs: produit matrice-vecteur, produit matrice-matrice, stencil 2D, etc.
– Ordonnancement de graphes de tâches avec et sans communications, avec ou sans contraintes de ressources: complexité, algorithmes d’approximations et heuristiques
– Analyse de dépendance et parallélisation automatique
– Exemple d’algorithme pour GPU
La note de contrôle continu est établie à partir d’un partiel organisé en milieu de semestre et d’un devoir à la maison de programmation.
L’objectif principal de ce cours est de présenter les techniques de base servant à l’évaluation qualitative et quantitative des performances de systèmes de communication et informatiques. L’accent sera mis sur les aspects théoriques mais sera illustré par l’analyse de plusieurs exemples de systèmes réels (réseaux de communication, de transport, de logistique). Ce cours comprendra aussi une introduction aux statistiques et abordera des questions de méthodologie expérimentale.
Plan indicatif :
Le but de ce cours est de présenter certains fondements des réseaux, dans son fonctionnement mais aussi des points de vues algorithmique et
d’évaluation de performances. Le module s’articule autour d’une présentation de l’architecture de l’Internet et des protocoles réseaux,
et des outils/méthodologie d’évaluation de performances. Les notions abordées lors de ce cours sont les suivantes :
Modalité d’évaluation
Le compilateur est un outil fondamental pour l’informaticien, qui se situe au coeur de tout développement informatique. Le but de ce cours est de donner aux étudiants une compréhension globale du fonctionnement d’un compilateur en présentant les aspects fondamentaux de la compilation de code natif pour les langages impératifs et à objets. Un accent particulier sera mis sur les méthodes d’analyse sémantique et d’optimisation de programmes utilisées dans les compilateurs récents (icc, gcc, etc). Ces notions de base seront complétées par un panorama des développements récents de la recherche dans le domaine. Enfin, on insistera sur la mise en oeuvre logicielle des différents aspects de la compilation à travers l’écriture d’un compilateur pour un langage impératif simple dans le cadre des travaux pratiques.
Voir la page www du cours.
Cet enseignement se focalise sur les aspects algorithmiques des systèmes distribués (ou répartis). La mise en œuvre d’algorithmes distribués pour résoudre les problèmes de communication, d’allocation de ressources et de synchronisation seront abordés. Ainsi les les problèmes d’élection de leader, les algorithmes à vagues, la détection de terminaison, les algorithmes de routages, la tolérance aux fautes, l’auto-stabilisation, etc. sont autant d’illustrations des points qui seront abordés dans cet enseignement. Différents types de mise en oeuvre de systèmes distribués seront également abordés au travers d’ERLANG, de CORBA ou encore de l’intergiciel DIET.
Anglais ou Français en fonction de la demande.
De plus en plus de domaines comme la biologie, l’analyse statistique ou l’apprentissage automatique, ont à traiter des données qui sont en fait des nuages de points dans des espaces de grandes dimensions. Ces données sont porteuses de caractéristiques topologiques et géométriques qui traduisent les propriétés des systèmes modélisés. Par exemple, la densité du nuage de points peut être concentrée autour d’une variété de dimension intrinsèque bien inférieure à celle de l’espace ambiant. Extraire une telle information n’est pas une tâche facile. Tout d’abord les données sont généralement bruitées, Ensuite, les structures et algorithmes de la géométrie algorithmique ont souvent des complexités exponentiellement croissantes en fonction de la dimension et passent mal à l’échelle pour ce type de données.
Ce cours propose une introduction à la géométrie algorithmique, axée sur les problématiques de l’approximation et de l’échantillonnage des objets géométriques. Il part de certains concepts classiques (enveloppe convexe, diagrammes de Voronoi) et aborde des méthodes récemment développées (core sets, persistance topologique) pour approcher les propriétés géométriques et topologiques des objets en dimensions supérieures, tout en évitant l’explosion exponentielle de la complexité, lié à la dimension.
Algorithmes pour l’approximation géométrique
Le cours ne suppose pas de prérequis. Toutes les notions fondamentales de géométrie algorithmique utilisées dans le cours seront exposées au préalable.
Il n’y a pas de frais d’inscription. Pour des questions d’organisation, il est toutefois nécessaire de s’inscrire en ligne ; [inscription fermée].
Tous les cours auront lieu dans l’amphithéatre B, au 3ème étage du bâtiment GN1 (bâtiment principal de la partie « sciences exactes » de l’ENS Lyon).
Un emploi du temps possible est le suivant:
Un certain nombre d’informations utiles se trouve sur la page principale des écoles de recherche en informatique fondamentale de l’ENS Lyon.
Tous les cours auront lieu dans l’amphithéatre B, au 3ème étage du bâtiment GN1 (bâtiment principal du site « Sciences » de l’ENS Lyon), ENS Lyon, 46 allée d’Italie, Lyon 7ème.
Lundi : Frédéric Maffray (9h30-12h45) ; Louis Esperet (14h-17h15)
Mardi : Louis Esperet (8h-10h) ; Andras Sebö (10h15-12h15)
Mercredi : Andras Sebö (8h-10h) ; Myriam Preissmann (10h15-12h15) ; Andras Sebö (14h-16h)
Jeudi : Myriam Preissmann (9h30-12h45)
Vendredi : Frédéric Maffray (9h30-12h45) ; Louis Esperet (14h-16h)
Cours 1 (Lundi 14h-17h15) Coloration vs. coloration par listes
Cours 2 (Mardi 8h-10h) Graphes sans triangles et coloration
Cours 3 (Vendredi 14h-16h) Coloration fractionnaire, coloration d’hypergraphes
Cours 1 (Lundi 9h30-12h45):
Cours 2 (Vendredi 9h30-12h45):
Cours 1 (Mercredi 10h15-12h15) :
Cours 2 (Jeudi 9h30-12h45) :
Cours 1 Mardi (10h15-12h15)
Cours 2 (Mercredi 8h-10h)
Cours 3 (Mercredi 14h-16h)
S’il y a des questions sur les exercices de la fiche fournie ci-dessus, vous pourrez les poser après le premier cours.
Bibliographie : Schrijver: Combinatorial Optimization; Lovász, Plummer: MatchingTheory; Lovasz: Combinatorial Problems and Exercises,
Voir la page des Ecoles du Master d’Informatique.
Eric Thierry (prenom.nom@ens-lyon.fr)
All the lectures will take place in amphitheater B, at the 3rd floor of the GN1 building (main building of the “exact sciences” part of ENS Lyon).
Schedule:
Afternoon: Corinne Touati 14h30 – 17h00
Notions from cooperative game theory: Bargaining and fairness.
Le but de cette partie est de comprendre comment appréhender les qualités d’une allocation (équilibre de Nash ou valeur optimisant une fonction par exemple). Nous commençons par la définition de la propriété d’optimalité. Parmi l’ensemble des points optimaux, un ensemble de critères permet de choisir un point dit équitable. Nous présentons des techniques numériques permettant d’approcher la frontière de Pareto et de calculer les points équitables. Enfin, nous verrons dans une dernière partie des méthodes d’évaluations des performances d’allocations, en terme à la fois d’équité et d’optimalité.
1. Optimalité
a. Définition de Pareto et notions liées
b. Propriétés des ensembles de Pareto (par ex. compacité)
c. Epsilon-approximation et méthodes de résolutions
d. Introduction à l’optimisation multi-critères, exemple d’un problème d’ordonnancement.
Afternoon: Eitan Altman 14:00 – 16:30
Convex games. These are games with a convex compact space. We shall study Rosen’s theory for the existence of an equilibria, The strict diagonal concavity property (which extends concavity to a game context). This notion is used to establish uniqueness of equilibrium in convex games.
We then introduce games with coupled constraints as in Rosen, as well as the related notion of generalized Equilibrium. These are equilibria in which the space of actions of each player are not independent: the actions available to a player may depend on those already chosen by others (for example, if there are capacity constraints over links then the amount of flow that a player can send over a link depends on how much other players send over that link). In the presence of such constrained there is in general no uniqueness of equilibrium. We thus introduce the problem of equilibrium selection. We introduce in particular the notion of normalized Nash equilibrium which and and relate it to scalable pricing.
Afternoon Rachid El-Azouzi 14:00 – 17:00
Super-modular Games and Potential Games. These are two classes of games in which not only do we know that equilibria exists, but we also know that sequence of best responses of players convenrge to the equilibrium. In particular, we show how potential games can be transformed into a global optimization problem whose optimum corresponds to the equilibrium of the original game.
Routing games Wardrop equilibrium: the players are modeled as infinitesimally small, which means that we have a continuum of players. computation of the equilibrium of the game
Definitions. Price of anarchy, price of stability, variational inequalities. Link between Nash and Wardrop equilibria.
Afternoon: Corinne Touati 14:00 – 17:00
Learning in games. All the previous evolutionary dynamics are related to learning process. The theory of learning in games explains the dynamic behavior of each player or agents depending on its own experience. Those learning processes related to the evolutionary dynamics, are used in order to construct distributed algorithms converging to equilibrium (Nash or ESS). We will introduce an example of distributed algorithm proposed in the literature which has been widely used in the networking community for power control, pricing, resource sharing and routing protocol. We will present other reinforcement learning algorithms: the Erev-Roth algorithm, and the Arthur algorithm for a variant of the last one with renormalization. Those distributed algorithms have interesting properties of implementation as they are totally distributed but they suffer from stability problems at the boundary of the state space. We will investigate how feedback delays and errors affect convergence
Afternoon: Eitan Altman 14:30 – 17:00
Introduction to Repeated Games. Threats and punishments. Credibility of threats and refinements of equilibria. Stochastic games and Dynamic programming approach for stochastic games. The discouted cost and the average cost games. Product stochastic games. Anonymous sequential games, Markov Decision Evoluationary Games.
Résumé du cours : Notre compréhension de ce qu'est un ordinateur (modèles de calculs) et de la manière dont il peut résoudre des problèmes mathématiques(algorithmique) est en évolution constante. Au-delà de l'approche traditionnelle, essentiellement fondée sur des systèmes déterministes et discrets (automates etc.) , une nouvelle vision émerge et qui se saisit des phénomènes probabilistes (aléatoire, approximation) et même des phénomènes quantiques (interférence, enchevêtrement) en les concevant non plus comme des difficultés à surmonter, mais comme de nouveaux outils offrant des perspectives remarquables. Quelles sont les limites de l'approche traditionnelle et qui sont franchies grâce à ces nouveaux outils? Jusqu'où peut-on éspèrer aller grâce à eux? Partie 1 (P.Arrighi, J.Degorre): Information quantique, causalité et automates cellulaires La physique quantique a précisément mis en évidence des phénomènes extrêmement utiles pour représenter, traiter et communiquer l'information. Ceci a donné lieu dans les 15 dernières années à de splendides résultats théoriques qui montrent que des performances quantitatives et qualitatives hors de portée de l'informatique classique deviennent alors possibles. Ainsi il est prouvé qu'un ordinateur quantique pourrait factoriser des nombres entiers en temps polynomial, ou bien rechercher un élément parmi une liste désordonnée de taille n en temps racine carrée de n. Ces résultats menacent la cryptographie moderne; mais ce que la physique quantique prend d'une main elle le redonne de l'autre. Ainsi des systèmes de transmission quantiques, déjà commercialisés, permettent d'obtenir une sécurité prouvée et inconditionnelle des communications. Ce cours effectuera d'abord tous les rappels nécessaires en algèbre linéaire. Les postulats de la mécanique quantique seront introduits, puis les principaux concepts et résultats connus et ayant trait à la nature particulière et non-locale de l'information quantique. Le cours sera alors axé vers la quête d'un modèle de calcul à la fois quantique et distribué, prenant en compte plusieurs des symmétries fondamentales de la physique (causalité, invariance par translation). C'est ce qui nous amènera à aborder des thèmes comme la causalité en mécanique quantique, les automates cellulaires dans un tel contexte, et la nature des relations entre physique et calcul.Plan: - Rappels d'algèbre linéaire - Postulats de la théorie quantique - Explorations sur la nature de l'information quantique (Algorithme de Deutsch, Non-disctinction d'états non-orthogonaux, No-cloning, Codage Super-dense, Téléportation) - Matrices de densité, opérateurs quantiques - Enchevêtrement quantique (classification, boîtes non-locales) - Opérateurs causaux et leur structure - Automates cellulaires : trois définitions et leur équivalence - définition axiomatique des automates cellulaires quantiques - théorèmes de structure - automates cellulaires quantiques universelsPartie 2 (F. Magniez): Algorithmique efficace Le but du cours est d'aborder les techniques permettant d'élaborer des algorithmes efficaces dans plusieurs contextes. Les techniques reposent sur des outils probabilistes et d'approximation. Les contextes modélisent les contraintes exercées sur la machine concernant ses ressources (temps, espace, aléa, requête, communication) et l'accès aux données (non contraint (random access) ou séquentiel (streaming)). Les domaines abordées seront donc : - Marches aléatoires : k-SAT, (s,t)-CONNECTIVITY dans RL - Graphes d'expansion (expander) : derandomizaton, (s,t)-CONNECTIVITY dans L - Algorithmes d'approximation (approximation du résultat) - Property testing (approximation sur l'entrée) - Théorème PCP (version light) : application à des preuves de non approximation - Streaming algorithms - One-way communication complexity : application a des preuves de non existence de streaming algorithms Correspondant local Pablo Arrighi
Linear logic was introduced by Jean-Yves Girard in 1986 as a
refinement of intuitionnistic logic. In the context of the
Curry-Howard correspondence between proofs and programs, linear logic
has renewed a lot of questions in proof theory in relation with the
semantics of programs.
Partly inspired by models of linear logic, game semantics provided in
1994 the first fully abstract model of the functional programming
language PCF. It has evolved towards the interpretation of various
additional programming features as well as applications to the
verification of programs.
These topics have evolved in two separate directions (proof theory for
linear logic, and programming semantics for game semantics) but with
many transfers of ideas between them along the past fifteen years.
The lectures will take place in “amphithéatre B”, at the 3rd floor of the GN1 building (main building at 46, allée d’Italie).
Tentative schedule:
On thursday, Febr. 11 afternoon, the
Choco seminar , on related topics, might also interest the participants.
Dan Ghica (University of Birmingham)
content:
Lorenzo Tortora de Falco (University of Roma 3)
Olivier Laurent (LIP – ENS Lyon)
content:
(LTdF: Lorenzo Tortora de Falco, OL: Olivier Laurent)
Course 2:
There are several useful informations on the main page of the research schools in Computer Science at ENS Lyon.
Plus d’informations sur: http://perso.ens-lyon.fr/florent.de.dinechin/beyond_the_pc.html