Master Mathématiques et applications

2ème année de Master Recherche
Spécialité : Mathématiques générales
Parcours : Mathématiques Discrètes et Fondements de l'Informatique

Université d'Aix-Marseille - Faculté des Sciences de Luminy

CNRS - IML

INRIA - Sophia Antipolis

Année 2013-2014

responsable David Kohel
secrétariatSonia Kerbache
correspondant Bernard Mourrain (INRIA Sophia-Antipolis)
adresse Département de Mathématiques,
163 avenue de Luminy, Case 901,
13288 Marseille Cedex 9
téléphone04 91 82 90 80
télécopie04 91 82 93 56
adresse électronique mdfi@iml.univ-mrs.fr
page web http://iml.univ-mrs.fr/MDFI/

Présentation générale

L'année MDFI est parcours de 2ème année de la spécialité Mathématiques générales du master Mathématiques et applications. Elle s'adresse aux étudiants titulaires d'une première année de master de mathématiques ou d'informatique (ex-maîtrise), ou d'un diplôme équivalent, et qui désirent recevoir une solide formation théorique avant d'aborder la recherche. La spécialité MDFI est sous la responsabilité de la Faculté des Sciences de Luminy de l'Université d'Aix-Marseille. L'effectif souhaité en deuxième année est d'environ 20 étudiants.

Programme de la deuxième année de master MDFI :

Première période (octobre-novembre-décembre)
quatre cours fondamentaux à choisir parmi six (25 heures/6 crédits chacun)
cours intensif d'une semaine à l'INRIA Sophia-Antipolis
Deuxième période (janvier-février)
deux options à choisir parmi celles proposées (25 heures/6 crédits chacune)
anglais (3 crédits)
Troisième période (mars-avril-mai-juin-...)
stage d'initiation à la recherche dans un laboratoire d'accueil du master MDFI (21 crédits) donnant lieu à la rédaction d'un mémoire et à une soutenance (vers la fin du mois de juin)

Tous les cours ont lieu à l'Institut de Mathématiques de Luminy, sauf le cours intensif, qui a lieu à Sophia Antipolis. Sur le site de Luminy, les étudiants ont accès à une salle équipée de postes de travail, et à la bibliothèque du CIRM (Centre International de Rencontres Mathématiques).

Les cours fondamentaux portent sur les structures discrètes de l'algèbre, de l'arithmétique, de la combinatoire, et de la logique. Les connaissances ainsi acquises sont utilisées dans les options, qui abordent les thèmes de recherche actuels, aussi bien en mathématiques qu'en informatique. En accord avec le responsable du master MDFI, les étudiants peuvent valider des options appartenant à d'autres spécialités du master Mathématiques et applications.

Double diplôme entre l'Université d'Aix-Marseille et Roma Tre

Le curriculum franco-italien de master en logique est un projet commun à l'Université d'Aix-Marseille et à l'Università di Roma Tre, dont l'objectif est de permettre à un petit nombre d'étudiants spécialisés en logique d'obtenir le double diplôme de

Ce curriculum est soutenu principalement par l'Université Franco-Italienne (UFI), ainsi que par l'Université d'Aix-Marseille, l'Institut de Mathématiques de Luminy et l'Università di Roma Tre.

Cours fondamentaux

Preuves et types

Lionel Vaux (IML-LDP)

Les travaux de Gentzen, et plus tard la découverte de l'interprétation algorithmique des preuves ont permis l'émergence d'une nouvelle discipline qui se donne pour but l'élaboration d'une théorie géométrique du calcul : la logique de la programmation. Celle-ci s'est développée de manière extrêmement vivante au point d'être aujourd'hui l'une des branches majeures de la logique mathématique.

Programme :

  • Déduction naturelle, calcul des séquents.
  • Lambda-calcul typé, correspondance de Curry-Howard.
  • Système F et théorème de normalisation forte de Girard.
  • Lambda-calcul pur.
  • Modèle de Engeler, sémantique cohérente.

Logique et théorie du calcul

Emmanuel Beffara (IML-LDP) et Yves Lafont (IML-LDP)

La théorie de la calculabilité s'intéresse essentiellement à la question suivante : au moyen d'un ordinateur, quelles fonctions peut-on calculer et quels problèmes peut-on résoudre ? Son développement est concomitant de l'apparition des principaux modèles de calcul (fonctions récursives, machines de Turing, lambda-calcul,...) et est très étroitement lié à öla logique mathématique : théorème d'incomplétude de Gödel (qui sera abordé dans ce cours), lambda-calcul typé (cours Preuves et types)...

La complexité cherche quant à elle à mesurer le degré de difficulté d'un problème, typiquement en termes de temps de calcul et d'espace utilisé. Il s'agit donc de questions plus fines, qui font l'objet de nombreuses recherches actuelles, notamment en rapport avec la logique.

L'objectif de ce cours est de présenter les outils et résultats fondamentaux pour aborder ces questions.

Programme :

  • Fonctions récursives, théorème de Kleene.
  • Machines de Turing, thèse de Church.
  • Arithmétique de Peano, théorème de Gödel.
  • Quelques méthodes et théorèmes de base en théorie de la complexité.

Bibliographie :

  • R. Cori, D. Lascar, Logique mathématique II : fonctions récursives, théorème de Gödel, théorie des ensembles, théorie des modèles, Axiomes, Masson, 1993.
  • J.-L. Krivine, Lambda-calcul, types et modèles, études et recherches en informatique, Masson, 1990.
  • C. Papadimitriou, Computational complexity, Addison-Wesley, 1994.

Algorithmique des graphes et réseaux

Victor Chepoi

L'objectif de ce cours est de présenter les notions élémentaires et les outils classiques intervenant en combinatoire dans l'étude des graphes. Dans une première partie, nous aborderons divers problèmes de graphes en nous intéressant plus particulièrement aux aspects algorithmiques et aux aspects constructifs.

Dans une deuxième partie nous étudierons des applications des outils théoriques à des problèmes de télécommunications. Les principaux sujets traités seront :

  • connexité, arbre couvrant de poids minimum, plus courts chemins, recherche en largeur et en profondeur ;
  • diamètre des réseaux, graphes de degré et diamètre bornés ;
  • graphes eulériens et graphes hamiltoniens, problème du voyageur de commerce et du postier chinois ;
  • flots, k-connexité (théorèmes de Menger), couplages parfaits et coloration.

Bibliographie

  • J. de Rumeur, Communication dans les réseaux de processeurs, Masson 1992.
  • D. West, Introduction to graph theory, Prentice Hall, 2001.
  • J.-A. Bondy & U.S.R. Murty, Graph theory with applications, American Elsevier, 1976.

Systèmes dynamiques

Pierre Arnoux (IML-DAC)

Ce cours introduit les concepts de base et les résultats fondamentaux de la théorie des systèmes dynamiques, du point de vue de la topologie (dynamique topologique) et de la théorie de la mesure (théorie ergodique).

  • Dynamique topologique (récurrence, transitivité, minimalité, mélange, entropie topologique).
  • Théorie ergodique (ergodicité, th?eorème ergodique, mélange faible et fort, théorie spectrale, entropie).
  • Rudiments de dynamique différentiable (exposants de Liapounoff, théorème d'Oseledets).
Ce cours comprendra de nombreux exemples, venant en particulier de l'arithmétique (fractions continues) et de la dynamique symboliques (mots infinis). On verra en particulier les propriétés élémentaires des échanges d'intervalles, dont les propriétés récemment démontrées seront le sujet du cours d'option de Pascal Hubert.

Bibliographie

  • Halmos, Ergodic theory (livre ancien, qui a l'avantage d'être court et d'aller très vite au coeur du sujet).
  • Katok-Hasselblatt, A first course in dynamics and introduction to the modern theory of dynamical systems.
  • Sinai Fomin Cornfeld, Ergodic theory
  • Pytheas Fogg, Substitutions in dynamics, arithmetics and combinatorics

Introduction aux courbes elliptiques et à la cryptographie elliptique

Stéphane Ballet (IML-ATI) et David Kohel (IML-ATI)

On présentera les notions suivantes :

  • Théorie de courbes elliptiques, surtout sur un corps fini.
  • Études de groupes de ces courbes.
  • Algorithme de Schoof et ses variantes.
  • Cryptographie elliptique.

Bibliographie

  • Lang, S. Elliptic functions. Graduate Texts in Mathematics, 112. Springer-Verlag, New York, 1987.
  • Koblitz, N. A course in number theory and cryptography. Springer-Verlag, New York, 1994.
  • Menezes, A. Elliptic curve public key cryptosystems. Kluwer Academic Publishers, Boston, MA, 1993.

Cours avancés

Sémantique dénotationnelle et logique linéaire

Luigi Santocanale (LIF) et Laurent Regnier (IML-LDP)

Cours fondamentaux conseillés : preuves et types, logique et théorie du calcul

Dans une première partie le cours présente la sémantique dénotationnelle à partir de la notion d'espace cohérent, qui est à l'origine de la logique linéaire, dont on étudiera les propriétés. On présentera notamment le calcul des séquents de la logique linéaire, ainsi que la notion de réseau de preuve, qui fournit une approche asynchrone de l'élimination des coupures.

On présentera d'autre part quelques aspects de la sémantique catégorique.

Bibliographie :

  • J.-Y. Girard, Proofs and Types, Cambridge Tracts in Theoretical Computer Science 7, Cambridge University Press, 1989. Accessible à partir de la page des publications de Yves Lafont.
  • R. Amadio, P.-L. Curien, Domains and lambda-calculi, Cambridge Tracts in Theoretical Computer Science 46, Cambridge University Press, 1998.

Décomposition des structures binaires

Pierre Ille (IML-LDP)

Cours fondamentaux conseillés :

En généralisant la notion usuelle d'intervalle d'un ordre total, on parvient à décomposer certaines structures combinatoires sous forme de quotients. On commencera par exposer le théorème de décomposition de T. Gallai pour les graphes non orientés. On l'adaptera ensuite à des graphes orientés comme les tournois. On le généralisera enfin aux structures binaires, encore appelées 2-structures étiquetées, qui regroupent tous les types de graphes. Le cours se terminera avec les premiers résultats sur les structures binaires indécomposables. La question générale étant : est-ce-qu'une structure binaire indécomposable admet des sous-structures indécomposables et de quelles tailles ?

Bibliographie :

  • A. Ehrenfeucht, T. Harju, G. Rozenberg, The Theory of 2-Structures, A Framework for Decomposition and Transformation of Graphs, (World Scientific, Singapore, 1999).
  • P. Ille, La décomposition intervallaire des structures binaires, La Gazette des Math\'ematiciens} 104 (2005), 39-58.
  • F. Maffray, M. Preissmann, A translation of Tibor Gallai's paper: Transitiv orientierbare Graphen, in: Perfect graphs, J.L. Ramirez-Alfonsin and B.A. Reed (Ed.), J. Wiley (2001) 25-66.

Dynamique symbolique

Pierre Guillon (IML-DAC)

Les sous-shifts de type fini sont des ensembles de mots infinis (sur un alphabet fini) évitant quelques motifs interdits. Nous allons voir que en dimension 1, les propriétés dynamiques sont assez bien comprises et reliées à la théorie des langages et à l'algèbre linéaire, alors qu'en dimension 2, ils correspondent aux pavages, et présentent des comportements très indécidables. En fonction des intérêts des étudiants, plusieurs ouvertures sont ensuite possibles : automates cellulaires (comme le jeu de la vie), pavages sur les groupes (finiment engendrés), langages d'images, calculabilité.

Algèbre, arithmétique et codage

Yves Aubry (IML-ATI) et David Kohel (IML-ATI)

Cours fondamentaux conseillés : , introduction aux courbes elliptiques et à la cryptographie elliptique

Nous commencerons par une étude de l'arithmétique sur les corps finis, des résultats les plus élémentaires à certains plus sophistiqués.

Nous enchaînerons par une présentation de la théorie des codes correcteurs d'erreurs.

Nous introduirons alors des éléments de géométrie algébrique et plus particulièrement les courbes sur les corps finis.

Enfin, nous terminerons par une étude des codes géométriques algébriques ainsi que des applications à la cryptographie.

Bibliographie :

  • Lidl, H. Niederreiter, Introduction to finite fields and their applications, Cambridge University Press.
  • F. J. Mac Williams and N. J. A. Sloane, The Theory of Error Correcting Codes, Amsterdam, The Netherlands, North-Holland, 1977.
  • R. Hartshorne, Algebraic Geometry, Graduate Texts in Math., Springer Verlag.

Mécanisation des preuves

Yves Bertot (INRIA-MARELLE), Loïc Pottier (INRIA-MARELLE) et Laurent Théry

Cours fondamentaux conseillés : preuves et types, logique et théorie du calcul

L'utilisation des lambda-calculs typés pour décrire la logique et les fondements de la théorie de la démonstration a donné naissance à la théorie des types, et à des systèmes d'aide au développement de preuves sur ordinateur basés sur une théorie typée. Nous nous intéresserons tout particulièrement au calcul des constructions inductives, un lambda-calcul typé d'ordre supérieur introduit par G. Huet, Th. Coquand et Ch. Paulin qui incorpore également des primitives de constructions récursives. Ces constructions se révèlent très utiles pour décrire aussi bien des objets mathématiques que la syntaxe et la sémantique des langages de programmation. Un tel calcul permet non seulement de vérifier des preuves de résultats mathématiques, mais également de certifier que des algorithmes remplissent des spécifications exprimables à l'aide du langage des types. Après une présentation des principes qui régissent le calcul des constructions inductives, le cours abordera les aspects pratiques de la mise en oeuvre de ce calcul dans un système (l'assistant à la preuve Coq) et étudiera quelques champs d'applications en mathématiques et en sémantique des langages de programmation.

Bibliographie :

  • G. Dowek, Théorie des types, Notes de cours.
  • Y. Bertot and Pierre Castéran, Interactive Theorem Proving and Program Development, Coq'Art the calculus of inductive constructions, Springer, 2004
  • L. Théry, A Machine-Checked Implementation of Buchberger's Algorithm, Journal of Automated Reasoning (2001) 26, pp. 107-137.

Calcul formel

Evelyne Hubert (INRIA-GALAAD) et Bernard Mourrain (INRIA-GALAAD)

Cours fondamentaux conseillés : , introduction aux courbes elliptiques et à la cryptographie elliptique

L'objectif de ce cours est de présenter quelques aspects constructifs de l'algèbre et leur utilisation pour la résolution de systèmes polynomiaux et différentiels.

Dans la première partie seront présentés des algorithmes fondamentaux sur les polynômes univariés (calcul de pgcd, factorisation, isolation de racines réelles,...) au travers desquels on apprendra les techniques de base (calcul modulaire, remontée de Hensel).

La seconde partie du cours sera consacrée aux systèmes de polynômes multivariés (bases de Gröbner, ensembles triangulaires, résultants, résolution de systèmes polynomiaux). Nous illustrerons ces méthodes par des applications pour la démonstration automatique en géométrie, en robotique, en vision par ordinateur, en traitement du signal ou en codage.

Bibliographie :

  • D. Cox, J. Little & D. O'Shea, Ideals, varieties and algorithms: an introduction to computational algebraic geometry and commutative algebra, Springer UTM, 1992.
  • J. von zur Gathen, Modern Computer Algebra, Cambridge Univ. Press, 1999.

Algorithmique des télécommunications

Frédéric Havet (INRIA-MASCOTTE), Nicolas Nisse (INRIA-MASCOTTE) et Frédéric Giroire (INRIA-MASCOTTE)

Cours fondamentaux conseillés :

Le but de ce cours est d'étudier divers problèmes se posant en télécommunications :

Réseaux tolérants aux pannes
réseaux embarqués dans les satellites et réseaux de flots expandeurs
Graphes aleatoires applications
modèles de graphes aléatoires
applications : modéliser les réseaux mobiles
graphe du web (pagerank, powerlaw, ...)
application détection d'anomalies
Jeux de capture dans les graphes (graph searching)
dualité avec stratégie du fugitif
décomposition linéaire (path decomposition)
équivalence des deux notions, monotonie, applications

Bibliographie :

  • A. Schrijver, Theory of linear and integer programming, John Wiley Sons, 1986.

Équipes

Institut de Mathématiques de Luminy

ATI (Arithmétique et théorie de l'information)

Cette équipe, dirigée par Gilles Lachaud, rassemble des chercheurs dont les travaux portent sur l'arithmétique et ses applications à la théorie de l'information.

L'arithmétique, c'est la théorie des nombres, c'est-à-dire l'étude des propriétés des entiers et de leurs généralisations : propriétés algébriques, algorithmiques, approximations diophantiennes, équations diophantiennes, etc. Dans cette discipline classique, les problèmes actuels se multiplient. Par exemple, l'approche des données irrationnelles et la quantification des distributions continues de données conduisent à l'étude des réseaux (maillages de l'espace) et des pavages de l'espace.

La théorie de l'information traite du problème suivant : comment décrire la structure d'un assemblage de données isolées ? Il s'agit aussi bien d'étudier des configurations régulières de points que de rendre compte de la manière dont un ordinateur traite et code l'information qu'on lui a confiée. En particulier, la théorie algébrique de l'information utilise l'arithmétique sur les corps finis (les champs de Galois) pour la correction des erreurs de transmission, la protection des données (cryptographie), la compression des fichiers, et l'élaboration de techniques de calcul comme la multiplication rapide.

DAC (Dynamique, arithmétique, combinatoire)

Cette équipe a une palette de thèmes de recherche très variée. L'idée centrale est d'explorer les rapports qu'entretiennent arithmétique, systèmes dynamiques, théorie des langages, et combinatoire. Un exemple frappant parmi d'autres : les suites sturmiennes sur un alphabet fini - celles dont le nombre de mots de longueur n vaut exactement n+1 - engendrent des systèmes dynamiques qui sont les bonnes représentations symboliques des rotations irrationnelles du cercle, et ceux-là seulement.

Parmi les thèmes relevant le plus exclusivement des mathématiques discrètes, on peut citer : les systèmes de numération (il n'y a pas que la représentation des nombres en base n), la combinatoire des mots, la transcendance en caractéristique non nulle, les méthodes de corps finis pour la génération de suites quasi-aléatoires, la combinatoire des graphes, et l'étude dynamique des automates cellulaires. On s'intéresse aussi aux rapports entre les mathématiques discrètes et d'autres sujets, que ce soit en géométrie, avec divers types de codage pour des systèmes classiques, ou en arithmétique. Tout cet ensemble recèle d'innombrables questions ouvertes, dont beaucoup ne sont même pas inventoriées.

LDP (Logique de la programmation)

L'équipe LDP, fondée par Jean-Yves Girard en 1992, étudie la théorie de la démonstration et ses applications à l'informatique. Cette discipline, qui est une branche de la logique mathématique, a été renouvelée par l'introduction de la logique linéaire. On peut distinguer trois axes de recherche :

  • La normalisation des preuves (beta-réduction du lambda-calcul). C'est la base de la programmation fonctionnelle (langage ML). On étudie les réseaux de preuve et leurs généralisations, les approches logiques de la complexité algorithmique, et depuis peu, les systèmes de logique linéaire différentielle. Dans une approche plus géométrique, l'équipe développe également un point de vue homotopique sur la réécriture, en utilisant des structures graphiques et catégoriques de dimension supérieure.
  • La sémantique des preuves. C'est la théorie mathématique du contenu algorithmique des preuves. On étudie la catégorie des espaces cohérents et ses généralisations. On développe également la géométrie de l'interaction, où les preuves sont interprétées dans des algèbres d'opérateurs (algèbres de Von Neumann, dans les travaux les plus récents de Jean-Yves Girard).
  • La recherche de preuve. C'est la base de la programmation logique (langage Prolog). On s'intéresse aux problèmes de prouvabilité et d'unification, à la programmation par contraintes, et à la démonstration assistée par ordinateur, avec en vue notamment les applications des théories logiques au traitement automatique du langage.

L'équipe s'intéresse également à certains problèmes de combinatoire des graphes et des structures ordonnées, notamment les problèmes de décomposition et de reconstruction.

INRIA - Sophia Antipolis

MASCOTTE (Méthodes algorithmiques, simulation, combinatoire et optimisation pour les télécommunications)

Mascotte (anciennement appelé SLOOP) est un projet commun avec le CNRS et l'Université de Nice-Sophia-Antipolis (UNSA) (dans le cadre du laboratoire I3S). L'objectif du projet Mascotte est de développer des méthodes et outils algorithmiques qui s'appliquent en particulier à la conception de réseaux de télécommunications. La réalisation de cet objectif implique la poursuite de recherches de haut niveau dans les domaines de l'algorithmique, de la simulation et des mathématiques discrètes.

GALAAD (Géométrie, algèbre et algorithmes)

Le projet GALAAD est consacré aux algorithmes algèbriques et géométriques et à leurs applications. Il se propose de rechercher des méthodes exactes et numériques pour le traitement de problèmes polynomiaux, de développer des outils logiciels adaptés, et de les appliquer dans différents domaines où apparaissent de tels problèmes, comme les robots parallèles, la vision, le traitement du signal, la géométrie des molécules. L'interaction constante entre algorithmiques, techniques d'implémentation et applications des méthodes est au coeur des activités de l'équipe. Parmi celles-ci, mentionnons :

  • algorithmique algébrique : élimination de variables, théorie des résidus algébriques, bezoutiens, résultants creux, variétés toriques ;
  • algorithmes en géométrie discrète pour exploiter la structure creuse des équations polynomiales : enveloppe connexe, polyèdre de Newton, volume des polytopes convexes et volume mixte, subdivision polyèdrique.
  • résolution exacte ou approchée d'équations et de systèmes polynomiaux : algèbre linéaire pour les polynômes - matrices structurées - fiabilité numérique ;
  • implémentation et application à des problèmes de robotique (robot parallèle), de vision (calibration, reconstruction 3D), de biologie moléculaire (reconstruction), de traitement du signal.

MARELLE (Logiciel et mathématiques)

Le projet MARELLE s'intéresse au développement de programmes corrects à partir de descriptions mathématiques des données, algorithmes, propriétés des objets mathématiques et des preuves de ces propriétés, en utilisant et éventuellement en étendant les outils fournis par le calcul des constructions inductives.

La réalisation de l'objectif du projet passe par trois grands thèmes :

  • la formalisation de théories mathématiques suffisamment large pour couvrir tous les objets mathématiques manipulés dans les programmes de calcul scientifique, par exemple les structures algébriques de groupes, anneaux, corps, espaces vectoriels ;
  • le développement d'outils facilitant le travail de preuve et permettant l'acquisition des compétences nécessaires par des mathématiciens et des ingénieurs ;
  • la form alisation d'algorithmes reconnus pour leur utilité dans le calcul scientifique : calcul sur les polynômes, les équations booléennes.