Admission

Prérequis : M1 spécialité mathématiques, informatique ou logique – ou équivalent.

Dossier : L'ouverture des inscriptions aura lieu le 1er mai 2019.

Débouchés

La suite naturelle de cette formation est la préparation d'un doctorat, soit en logique mathématique, soit en informatique (notamment fondamentale).

Organisation

Un semestre de cours fondamentaux, un semestre de cours avancés, un stage d'initiation à la recherche.

Organisation

Le LMFI est composé :

  • Au premier semestre :
    • un cours préliminaire intensif de logique (30h), facultatif;
    • un tronc commun constitué de quatre cours fondamentaux (trois cours de 48h, un cours de 84h);
    • les groupes de travail des cours fondamentaux (36h chacun).
  • Au second semestre :
    • huit cours avancés (48h chacun);
    • des cours d'ouverture (24h chacun);
    • une initiation à la recherche sous forme d'un stage/mémoire, encadré par un enseignant-chercheur.

À la demande des élèves, les cours pourront être donnés en anglais.

Stage d'initiation à la recherche

Le stage/mémoire de M2 peut s'effectuer, avec l'accord des responsables, soit :

Étudier à l'étranger

contact : Tamara Servi

Programme Erasmus+

Le LMFI a des partenariats avec les groupes de logique dan de nombreuses université européennes (Turin, Münster, Pisa, Freiburg, Florence...). Grâce au programme d'échange Erasmus+, les étudiants et enseignants des universités partenaires peuvent prendre part aux activités du LMFI. De même les étudiants et enseignants du LMFI peuvent prendre part aux activités de nos universités partenaires. La liste de toutes les universités partenaires de l'Université Paris Diderot peut être trouvée ici.

Erasmus+ vers le LMFI : Les étudiants en master des universités partenaires peuvent postuler pour étudier au LMFI (au 1er semestre, 2nd semestre, ou les deux). Les procédures et dates limites dépendent des universités partenaires (prendre contact avec un professeur de logique ou la personne responsable des échanges internationaux dans votre université).

Erasmus+ depuis le LMFI : Les étudiants de M1 à Paris Diderot ainsi que les étudiants du LMFI peuvent postuler à un échange dans une des université partenaire (4 à 10 mois). Pour plus de détails (procédures, dates, choix de destination, etc.) prendre contact avec Tamara Servi.

Stage de recherche (mémoire de master)

Vers le LMFI : Les étudiants de master dans une université étrangère qui souhaitent faire un stage de recherche (mémoire de master) à l'Université Paris Diderot peuvent prendre contact avec Boban Velickovic et Christine Tasson.

Depuis le LMFI : Les étudiants du LFMI ont aussi la possibilité de faire leur stage (mémoire de master) dans une université étrangère (ou en codirection entre Paris et l'étranger). Les étudiants intéressés peuvent prendre contact avec Tamara Servi.

Calendrier

  • 2 au 13 septembre 2019 : cours préliminaire intensif de logique;
  • 16 septembre au 6 décembre 2019 : cours fondamentaux;
  • 16 au 20 décembre 2019 : examens du premier semestre;
  • 6 janvier au 27 mars 2019 : cours avancés et d'ouverture;
  • 20 au 24 avril 2019 : examens du deuxième semestre;
  • à partir du 15 avrilet avant le 30 septembre 2020 : stage/mémoire d'introduction à la recherche.

Le planning du 1er semestre peut être trouvé ici.

Validation

La validation du M2 LMFI correspond à l'acquisition de 60 crédits ECTS selon les modalités suivantes :

  • Validation des quatre cours fondamentaux (20 ECTS).
  • Validation de deux cours avancés (8 ECTS chacun).
  • Validation de 8 ECTS d'ouverture, qui peuvent être obtenues, au choix par :
    • par la validation de deux cours d'ouverture (4 ECTS chacun);
    • par la validation d'un troisième cours avancé (8 ECTS)
  • Le stage est crédité de 16 ECTS.

Les cours d'ouverture sont à choisir dans la liste proposée par le M2 ou, après accord des responsables, parmi des unités d'un autre M2, par exemple dans le M2 Mathématiques Fondamentales ou dans le MPRI (Master Parisien de Recherche en Informatique).

Cours proposés

1er Semestre

Cours préliminaire de logique

0 ECTS, semestre 1

Prérequis
Validationsans
EnseignantPatrick Simonetta et Pierre Letouzey
Horaires hebdomadaires 18 h CM

Syllabus

Le cours préliminaire sera du 2 au 13 septembre.

  • Calcul des propositions : tables de vérité, tautologies, formes normales, compacité.
  • Calcul des prédicats : langages du premier ordre, termes, formules, modèles ; satisfaction d’une formule dans un modèle ; sous-structures ; isomorphismes ; équivalence élémentaire.
  • Théorie des ensembles : axiomes de Zermelo-Frænkel ; cardinaux ; théorèmes de Cantor et de Cantor- Bernstein ; ensembles finis, ensembles dénombrables.
  • Introduction à la programmation : Mise à niveau en programmation fonctionnelle Ocaml ; Lien avec le lambda-calcul, récursivité, typage ML ; structures de données usuelles (booléens, entiers, listes, options, arbres, ...).

Théorie des modèles

4 ECTS, semestre 1

Prérequis
Validationexamen
EnseignantTomás Ibarlucia
Horaires hebdomadaires 2 h CM , 2 h TD

Syllabus

  • Ultraproduits, compacité.
  • Extensions élémentaires, Théorèmes de Lowenheim-Skolem.
  • Méthode des diagrammes, théorèmes de préservation.
  • Va et vients, élimination des quantificateurs.
  • Espace des types, théorème d'omission des types, modèles kappa-saturés, modèles atomiques.
  • Théories oméga-catégoriques, théorème de Ryll-Nardzewski. Décidabilité de quelques théories axiomatiques.

Théorie des ensembles

4 ECTS, semestre 1

Prérequis
Validationexamen
EnseignantFrançois Le Maître
Horaires hebdomadaires 2 h CM , 2 h TD

Syllabus

  • ordinaux, récurrence transfinie ;
  • axiome du choix et énoncés équivalents ;
  • arithmétique des cardinaux infinis ; cofinalité, cardinaux réguliers et singuliers, théorème de König ;
  • la hiérarchie de von Neumann, théorèmes de réflexion ;
  • filtres et ultrafiltres, ensembles stationnaires dans $\omega_1$, lemme de Fodor ;
  • relations bien fondées et collapse de Mostowski ;
  • quelques éléments de la théorie descriptive.

Théorie de la démonstration

4 ECTS, semestre 1

Prérequis
Validationexamen
EnseignantThierry Joly
Horaires hebdomadaires 2 h CM , 2 h TD

Syllabus

  • Théorème de complétude du calcul des séquents égalitaire LK par les témoins de Henkin.
  • Calcul des séquents : Élimination des coupures et théorème du séquent médian dans LK. Théorème de Herbrand. Sous-calcul LJ : la logique intuitionniste et son interprétation BHK. Propriétés de la sous-formule et du témoin existentiel dans LJ.
  • Déduction naturelle : Systèmes NK et NJ. Élimination des coupures de NJ. Propriétés de la sous-formule et du témoin existentiel dans NJ, puis dans HA (arithmétique intuitionniste).
  • Lambda-calcul : Propriétés de confluence et de standardisation. Représentation des fonctions récursives. Système T. Correspondance de Curry-Howard. Réalisabilité, normalisation forte et correction des programmes.

Calculabilité et incomplétude

8 ECTS, semestre 1

Prérequis
Validationexamen
EnseignantPaul Rozière et Hervé Fournier
Horaires hebdomadaires 4 h CM , 2 h TD

Syllabus

  • Calculabilité : fonctions récursives et fonctions calculables par machine ; caractérisation logique des fonctions calculables ; théorème smn et théorèmes de point fixe ; notions de réduction et problèmes indécidables.
  • Introduction à la complexité : classes en temps et espace, théorèmes de hiérarchie, réductions, complétude, circuits booléens, introduction à la complexité algébrique.
  • Arithmétique formelle : axiomes de Peano et sous-systèmes faibles ; arithmétisation de la logique ; théorèmes d’indécidabilité ; les théorèmes d’incomplétude de Gödel.

Théorie des Catégories

4 ECTS, semestre 1

Prérequis
Validationexamen
EnseignantFrancois Metayer
Horaires hebdomadaires 2 h CM

Syllabus

Le cours présente les concepts fondamentaux de la théorie des catégories, illustrés de nombreux exemples. L’objectif essentiel est préparer l’accès aux applications actuelles des catégories en logique, en informatique théorique et en théorie de l’homotopie.

2nd Semestre

Théorie des modèles : Outils classiques

8 ECTS, semestre 2

PrérequisEn plus des notions de théorie des modèles du cours du premier semestre, des notions que l’on apprend typiquement au cours de la licence de mathématiques pourront être utiles pour comprendre les exemples et les applications.
Validationexamen
EnseignantTamara Servi
Horaires hebdomadaires 4 h CM

Syllabus

Ce cours sera une continuation naturelle du cours de théorie des modèles du premier semestre : au premier semestre, étant donnée une L-structure M, vous allez identifier les L-énoncés qui sont vrais dans M (i.e. la théorie de M). Inversement dans ce cours, étant donnée une L-théorie complète T, nous allons classifier ses modèles à isomorphisme près.

Théorie des modèles des corps pseudo-finis

8 ECTS, semestre 2

PrérequisThéorie de Galois. Des rudiments de théorie des modèles et de géométrie algébrique pourront être utiles. Des rappels seront fait en cours, si besoin.
Validationexamen
EnseignantSilvain Rideau
Horaires hebdomadaires 4 h CM

Syllabus

L’étude des propriétés asymptotiques des corps finis, c’est à dire les propriétés vraies dans tous les corps finis suffisamment grands, se fait naturellement par le biais des corps dits pseudo-finis : les modèles infinis de l’ensemble des énoncés vrais dans tous corps finis. Cette classe a été définie et étudiées par Ax et il en a donné une caractérisation algébrique : ce sont les corps parfaits, pseudo- algébriquement clos qui ont exactement une extension de chaque de degré.

Les structures pseudo-finies ont plus récemment joué un rôle déterminant dans l’approche, par la théorie des modèles, de certaines questions combinatoires, entre autre dans les travaux de Hrushovski en combinatoire additive. Ces derniers trouvent une partie de leurs racines dans les résultats de Chatzidakis, van den Dries et Macintyre qui ont donné une description fine des ensembles définissables dans les corps pseudo-finis en exhibant, entre autre, un équivalent pseudo-fini de la mesure de comptage.

Le but de ce cours sera d’introduire les résultats d’Ax et de Chatzidakis-van den Dries- Macintyre ainsi que les notions algébriques nécessaires à leur compréhension. Enfin, on abordera, dans la mesure du possible, des questions liées à la théorie géométrique des modèles comme l’étude des groupes définissables ou des imaginaires ainsi que des questions de classification.

Théorie des ensembles : Outils classiques

8 ECTS, semestre 2

Prérequis
Validationexamen
EnseignantBoban Velikovic
Horaires hebdomadaires 4 h CM

Syllabus

Le 8 août 1900, lors du second Congrès International des mathématiciens, à Paris, David Hilbert énonça une liste de 23 problèmes mathématiques qui, selon lui, devaient servir de guide pour les recherches à venir dans le nouveau siècle. Le premier problème de cette liste, l’hypothèse du continu de Cantor, a été résolu, en deux temps : par Gödel (1938) qui construisit un modèle interne de l'hypothèse généralisée du continu, et par Paul Cohen (1963), qui a inventé une construction de modèle pour la négation de l’hypothèse de Cantor. Ce cours couvrira principalement les deux constructions de modèles de la théorie des ensembles introduites par Gödel et Cohen.

Théorie descriptive des ensembles

8 ECTS, semestre 2

Prérequis
Validationexamen
EnseignantDominique Lecomte
Horaires hebdomadaires 4 h CM

Syllabus

En théorie descriptive des ensembles classique, on s’intéresse aux ensembles apparaissant naturellement dans divers domaines des mathématiques, notamment l’analyse fonctionnelle, l’analyse harmonique, les systèmes dynamiques ou encore la théorie des groupes. Un des objectifs est d’étudier leur complexité topologique. Par exemple, on peut classifier les sous-ensembles boré́liens des réels selon le nombre d’étapes qui sont nécessaires pour les obtenir à partir d’ensembles ouverts en effectuant des unions dénombrables et des passages au complémentaire.

Le cadre général est celui des espaces topologiques polonais, où le théorème de Baire est un outil puissant. On s’intéressera d’abord aux sous-ensembles boréliens des espaces polonais, dont on verra qu’ils sont naturellement hiérarchisés par les ordinaux dénombrables. Ensuite viennent les images via une application borélienne de boréliens (ensembles analytiques) et leurs complémentaires (ensembles co-analytiques). On verra notamment une méthode permettant de montrer qu’un ensemble est co- analytique mais non borélien.

Le cours se terminera par une introduction à la théorie descriptive effective des ensembles et à ses applications. Un de ses outils très puissants est la topologie de Gandy-Harrington, et nous établirons ses propriétés permettant son utilisation dans la preuve de nombreux résultats de dichotomie. Nous détaillerons trois exemples, les dichotomies d’Hurewicz, Silver et Kechris-Solecki-Todorčević. Nous énoncerons d’autres exemples plus récents, en détaillant suivant le temps disponible.

Preuves et programmes : Outils classiques

8 ECTS, semestre 2

Prérequis
Validationexamen
EnseignantAlexis Saurin et Christine Tasson
Horaires hebdomadaires 4 h CM

Syllabus

La théorie de la démonstration a connu au moins deux évolutions majeures au cours du siècle dernier suite aux théorèmes d'incomplétude de Gödel. La première a eu lieu dans les années 30, immédiatement après les résultats d'incomplétude, avec l'introduction et l'étude de la déduction naturelle et du calcul des séquents par Gentzen et du lambda-calcul par Church. Church montrait alors l'indécidabilité du calcul des prédicats via le lambda-calcul tout en introduisant un modèle de calcul universel tandis que Gentzen déduisait la consistance de divers systèmes logiques comme corollaire de l'élimination des coupures en calcul des séquents.

La seconde étape a eu lieu dans les années 60 avec la mise en évidence progressive, par le biais de la correspondance de Curry-Howard, des liens profonds entre preuves et programmes, depuis la correspondance entre lambda-calcul simplement typé et déduction naturelle propositionnelle minimale jusqu'aux diverses extensions de cette correspondance au second ordre, à la logique classique et jusqu'à l'émergence de la notion de linéarité en théorie de la démonstration. La logique linéaire a profondément renouvelé les liens entre la sémantique formelle des langages de programmation d'un côté et la théorie de la démonstration de l'autre. L'algèbre linéaire s'impose comme troisième pôle de cette correspondance, en mettant au centre la notion de ressource du calcul.

Le cours fondamental a traité de la première étape. Ce cours sera consacré aux développements depuis les années 60 et présentera les outils classiques pour l'étude de la correspondance de Curry-Howard. Après quelques rappels et compléments du cours fondamental, le cours se concentrera sur deux concepts fondamentaux, le second-ordre et la linéarité, et à leurs développements, notamment dans un cadre algébrique. On appliquera notamment les résultats du cours à l'étude de PCF, un langage de programmation idéalisé.

Théorie homotopique des types

8 ECTS, semestre 2

PrérequisLa participation aux cours d'introduction à la programmation et la preuve formelle en Coq, ou la maîtrise des notions correspondantes, est un prérequis pour ce cours.
Validationexamen
EnseignantHugo Herbelin
Horaires hebdomadaires 4 h CM

Syllabus

Théorie des types de base:

  • Système de types purs
  • Théorie des types de Martin-Löf
  • Calcul des constructions inductives
  • La correspondance preuve/programme
  • Discernabilité et indiscernabilité des preuves − Types inductifs et coinductifs
  • Extensionalité en théorie des types

Théorie des types homotopique :

  • La correspondance type/espace, égalité/chemin
  • Concepts homotopiques en théorie des types (espaces contractibles, h-niveaux, univalence, systèmes de factorisation faibles, fibrations, cofibrations)
  • Type inductifs supérieurs (sphères, quotients, troncations,...)
  • Axiome du choix et logique classique en théorie des types homotopique

Modèles :

  • Catégories de famille
  • Théorie des types cubique − Traductions internes
  • ω-groupoïdes
  • Complexes de Kan

Programmation fonctionnelle et preuves formelles en Coq

8 ECTS, semestre 2

Prérequis
Validationprojet
EnseignantPierre Letouzey
Horaires hebdomadaires 2 h CM , 2 h TP

Syllabus

Attention, ce cours aura lieu les 6 dernières semaines du 1er semestre et les 6 premières semaines du 2nd semestre.

Une moitié des heures de ces modules consistera en des cours, l’autre en des TP sur machine. Ces cours se concluront par un projet à réaliser en Coq. Le contenu de ces cours est un prérequis pour le cours de théorie des types homotopiques.

Complexité descriptive : du discret au continu

8 ECTS, semestre 2

PrérequisOn fera l’hypothèse que les étudiants connaissent les bases de la calculabilité (récursion primitive notamment) et de la complexité (P, NP).
Validationexamen
EnseignantOlivier Bournez et Arnaud Durand
Horaires hebdomadaires 4 h CM

Syllabus

L’objectif du cours est de présenter plusieurs point de vue sur la complexité venant de la logique, de la théorie de la récursion ou de l’analyse. Ces approches ont pour point commun de s’abstraire de la notion de machine (et de ses mesures associées comme le temps et l’espace) au profit d’une vision plus descriptive du calcul. Le cours vise notamment à étudier des formalismes logiques sous l’angle de leur pouvoir d’expression et à présenter de multiples caractérisations des classes de complexité usuelles.

Ces approches de le complexité dîtes descriptives ou implicites ont connu des applications importantes en théorie des bases de données, des langages de programmation ainsi que plus récemment autour de l’analyse des systèmes d’équations différentielles, ou autour de la compréhension de la puissance de modèles alternatifs de calculs basés sur la bioinformatique, ou le calcul analogique.

On visera à présenter dans un premier temps des résultats sur la complexité classique [8, 13], pour aller vers des extensions à des modèles algébriques comme le modèle de Blum Shub et Smale [3, 2], à espace continus comme les modèles de réseaux de neurones/deep learning [17], puis à temps et espace continu comme le modèle de Shannon [16].

Blockchains, tokens and contracts

4 ECTS, semestre 2

Prérequis
Validationexamen
EnseignantVincent Danos et Ilias Garnier
Horaires hebdomadaires 2 h CM

Syllabus

Ce cours vise à présenter les fondements informatiques des blockchains (protocoles de communications, théorie des jeux), ainsi que des exemples de protocoles mis en oeuvre en particulier dans les cryptomonnaies et les smart-contracts.

Histoire et Philosophie de la Logique

4 ECTS, semestre 2

Prérequis
ValidationCC+examen
EnseignantBrice Halimi
Horaires hebdomadaires 2 h CM

Syllabus

En quoi la logique est-elle formelle ?

Le cours sera consacré à cette question. Il examinera en particulier trois grandes raisons de déclarer « formelle » la logique : parce qu’elle recourt à des ressources discursives qu’on peut dire formelles (schématiques) ; parce qu’elle porte sur des formes (dont le statut est à préciser : « constantes logiques » pour Russell, « formes dérivées du quelque chose en général » pour Husserl, pour prendre deux exemples importants) ; parce qu’elle vise à une validité indépendante de tout contenu particulier (logique comme science universelle).

Ces trois grandes raisons ne sont pas nécessairement compatibles. Par ailleurs, l’examen de la question posée impliquera bien entendu la prise en compte de l’histoire de la logique, et une réflexion sur la situation de la logique entre philosophie et mathématiques. Ce sera l’occasion d’examiner l’enjeu de la « généralité absolue », c’est-à-dire celui de la possibilité d’une théorie portant sur absolument toutes choses en général.

Compétences visées : connaissance des enjeux philosophiques de l’histoire de la logique au XXe siècle.

Admission

Le candidat devra avoir validé une 1ère année de Master (M1), une Maîtrise ou un titre équivalent. Cette première année devra avoir été effectuée dans une spécialité mathématique, informatique, ou logique.

Candidature des étudiants étrangers

Afin de faciliter la mobilité internationale, l’Université Paris Diderot adhère à l’Agence Campus France. Les étudiants étrangers intéressés pourront trouver les détails de la procédure sur leur site. Les étudiants de pays relevant de la procédure Étude en France doivent candidater auprès de cet organisme avant mars 2019.

Pour toutes les autres candidatures

Les étudiants doivent déposer une demande de pré-inscription sur le site de l'université (https://candidaturesca19mprod.app.univ-paris-diderot.fr/ca19m/#!accueilView), puis transmettre par voie postale le dossier de préinscription avec les pièces justificatives.

Bourses

Quelques informations sur les possibilités de bourses pour l'entrée en M1 ou M2 notamment à destination des étudiants étrangers :

Dates importantes:

  • mars 2019 : pour les étudiants devant effectuer la procédure Étude en France, voir le site de Campus France pour les détails. Cela ne concerne pas les étudiants déjà inscrits dans un établissement universitaire en France ou ressortissant d'un état membre de l'union européenne.
  • Du 1er mai au 10 juillet 2019 : dépôt de dossier d'inscription sur le site E-candidat (voir détails ci-dessus).
  • Du 25 août au 15 septembre 2019 : dépôt de dossier d'inscription sur le site E-candidat pour un examen de votre candidature à la session septembre.
  • Du 2 au 13 septembre 2019 : cours préliminaire facultatif.
  • 16 septembre 2019 : début des cours fondamentaux.

Débouchés

La suite naturelle de cette formation est la préparation d'un doctorat, soit en logique mathématique, soit en informatique (notamment fondamentale). Pour un doctorat en informatique, la thèse peut éventuellement être préparée dans une entrerpise ou un organisme public de recherche (INRIA, CEA, ONERA, etc.). Ces dernières années, plus de la moitié des étudiants validant le M2 continuent en thèse.

Les débouchés principaux après le M2 et la thèse sont dans la recherche au sens large :

  • dans le milieu universitaire (français ou étranger) ou des organismes publics de recherche (CNRS, INRIA, CEA, ONERA, etc.);
  • dans les services de recherche et développement d'entreprises du monde industriel (EDF, France Telecom, Siemens, EADS, etc.). Les services de recherche et développement sont particulièrement demandeurs d'étudiants ayant une forte compétence à la fois mathématique, logique et informatique, leur permettant d'encadrer des ingénieurs travaillant dans les domaines de la certification de logiciels, de la vérification de programmes et de protocoles et plus généralement dans la sécurité informatique. Dans certains cas, le recrutement peut s'effectuer directement à l'issue du Master.

Informations pratiques