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 2014-2015

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 Marseille et l'Università di Roma Tre.

Cours fondamentaux

Preuves et types

Lionel Vaux (I2M-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 (I2M-LDP) et Yves Lafont (I2M-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 et complexité

Nadia Creignou (LIF-ACRO) et Victor Chepoi (LIF-ACRO)

Principales techniques de conception et analyse d'algorithmes (efficaces) pour les problèmes polynomiaux et les problèmes NP-complets. Complexité de l'approximation, du comptage. Complexité paramétrée. Classes probabilistes.

Systèmes dynamiques

Pierre Arnoux (I2M-GDAC)

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éorè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

Cryptographie symétrique

Serge Vladuts (I2M-ATI)

  • Bref tour d'horizon des systèmes cryptographiques classiques fondés sur les substitutions ou les permutations qui permettent de comprendre les principes des systèmes modernes de chiffrement.
  • Quelques systèmes actuels de cryptographie symétrique: chiffrement à flot, chiffrement par blocs.
  • Diverses attaques qu'on peut mener contre ces systèmes: attaques par corrélation, algébriques, différentielles, linéaires...
  • Les contre-mesures: utilisation de fonctions booléennes résistantes aux attaques.

Bibliographie

  • P. Barthélemy, R. Rolland, P. Véron, Cryptographie principes et mises en oeuvre, Lavoisier, 2005.
  • C. Carlet, Boolean Functions for Cryptography and Error Correcting Codes, chapitre de la monographie Boolean methods and models publiée prochainement par Cambridge University Press (Peter Hammer et Yves Crama éditeurs). Version préliminaire.
  • C. Carlet, Vectorial (multi-output) Boolean Functions for Cryptography. Idem. Version préliminaire.
  • David R. Kohel, Cryptography
  • G. Zemor, Cours de Cryptographie, Cassini, 2000.

Cours avancés

Sémantique dénotationnelle et logique linéaire

Luigi Santocanale (LIF-MOVE) et Laurent Regnier (I2M-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.

Équipes

Institut de Mathématiques de Marseille

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

Cette équipe 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.

GDAC (Géométrie, Dynamique, Arithmétique, et 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

COATI (Combinatorics, Optimization, and Algorithms for Telecommunications)

COATI (anciennement appelé Mascotte) 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 COATI 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.

Laboratoire d'Informatique Fondamentale

ACRO (Algorithmique, Combinatoire et Recherche Opérationnelle)

L'activité de recherche concerne principalement l'optimisation combinatoire (complexité, méthodes et algorithmes de résolution, programmation en nombres entiers, applications à la Recherche Opérationnelle), la théorie des graphes (structure, métrique et algorithmique des graphes et réseaux), la combinatoire (systèmes d'ensembles structurés), et la géométrie discrète et algorithmique (géométrie des distances, distances de chanfrein).

MOVE (Modélisation et Vérification)

L'équipe MOdélisation et VErification (MOVE) à Luminy est une équipe du LIF. Le concept de système distribué est fondamental tant pour les applications pratiques que pour les fondements théoriques de l'informatique. La conception d'applications correctes et sûres dans ce cadre est particulièrement difficile. La recherche de l'équipe MoVe est motivée par ce problème et l'objectif de l'équipe est de faire progresser les concepts fondamentaux dans ce domaine, mais également de développer des outils logiciels permettant de tester nos approches. Les thématiques de recherche de l'équipe sont organisées suivant deux axes : l'axe Vérification et l'axe Logique, automates et combinatoire.