Archive 2022

Admission

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

Dossier : L'ouverture des inscriptions aura lieu le 3 mai 2021.

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 : Tomás Ibarlucía

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 Tomás Ibarlucía.

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 Antonio Bucciarelli.

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 Tomás Ibarlucía.

Calendrier 22/23

  • 29 août au 9 septembre 2022 : cours préliminaire intensif de logique;
  • 12 septembre au 2 décembre 2022 : cours fondamentaux;
  • 12 au 16 décembre 2022 : examens du premier semestre;
  • 2 janvier au 24 mars 2023 : cours avancés et d'ouverture;
  • 3 au 7 avril 2023 : examens du deuxième semestre;
  • à partir du 10 avril et avant le 29 septembre 2023 : stage/mémoire d'introduction à la recherche.

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

  • 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
EnseignantTomas Ibarlucia
Horaires hebdomadaires 2 h CM , 2 h TD

Syllabus

  • Langages, structures, théories du premier ordre
  • Ultraproduits, compacité.
  • Extensions élémentaires, Théorèmes de Lowenheim-Skolem, chaînes élémentaires.
  • Théorèmes de préservation.
  • Va et vients.
  • Élimination des quantificateurs, modèle-complétude.
  • Espace des types.
  • (Si le temps le permet) Typer réalisés et types omis, modèles atomiques.

Théorie des ensembles

4 ECTS, semestre 1

Prérequis
Validationexamen
EnseignantAlessandro Vignati
Horaires hebdomadaires 2 h CM , 2 h TD

Syllabus

  • Les axiomes de ZF
  • Ordinaux, Cardinaux, récurrence transfinie
  • Arithmétique ordinaux et cardinaux
  • Axiom du Choix et équivalents, filtres et ultrafiltres
  • Cofinalité, cardinaux réguliers/singuliers, théorème de König
  • Ensembles stationnaires, clubs, Lemma de Fodor
  • Absoluité et théorèmes de reflexion
  • L'universe constructible

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
EnseignantArnaud Durand
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.

Programmation fonctionnelle et preuves formelles en Coq

8 ECTS, semestre 1

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

Syllabus

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.

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
EnseignantElisabeth Bouscaren
Horaires hebdomadaires 4 h CM

Syllabus

Ce cours sera une continuation naturelle du cours de théorie des modèles du premier semestre. On cherchera à comprendre et classifier les modèles d'une théorie du 1er ordre donnée à travers les types que l'on peut réaliser ou omettre.

Géométrie o-minimale

8 ECTS, semestre 2

Prérequis
Validationexamen
EnseignantTamara Servi
Horaires hebdomadaires 4 h CM

Syllabus

En termes modèle-théoriques, une expansion M du corps ordonné des réels est o-minimale si tout sous-ensemble M-définissable de R a un nombre fini de composantes connexes. Ceci peut être également formulé en des termes purement géométriques, en tant que propriété d'une collection d'ensembles réels stable par les opération booléennes ensemblistes, produits cartésiens et projections linéaires. Les ensembles définissables dans une structure o-minimale partagent de nombreuses bonnes propriétés topologiques avec les ensembles algébriques et analytiques réels (théorie de la dimension, finitude uniforme, stratification), d'où l'intérêt pour la géométrie o-minimale en lien avec la géométrie Diophantienne et arithmétique, les systèmes dynamiques non-oscillants et l'analyse asymptotique. Je donnerai une vue d'ensemble des résultats principaux sur les structures o-minimales et ensuite j'illustrerai les principales méthodes pour démontrer qu'une collection de fonctions réelles engendre une structure o-minimale. Il n'y a essentiellement pas de prérequis pour ce cours, outre que les notions de base d'algèbre et d'analyse acquises en licence : les notions de théorie de modèles nécessaires sont minimales et je fournirai de la bibliographie sur le sujet si besoin.

Théorie des ensembles : Outils classiques

8 ECTS, semestre 2

Prérequis
Validationexamen
EnseignantBoban Velickovic
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.

L’équilibre stratégique en logique : les jeux et les modèles

8 ECTS, semestre 2

Prérequis
Validationexamen
EnseignantMirna Dzamonja
Horaires hebdomadaires 4 h CM

Syllabus

Le thème principal du cours est l’interaction entre la logique et les jeux. De nombreux exemples d’une telle interaction existent, notamment la clôture stratégique et la détermination en théorie des ensembles, les jeux de Ehrenfeucht-Fraïssé en théorie des modèles, le jeux des cailloux en complexité descriptive et d’arguments de décision en théorie d’automates. Pour citer Jouko Väänänen, il y a trois sortes de jeux en logique, les trois en connexion étroite. Il nomme cette connexion « l’équilibre stratégique en logique ». Le cours sera librement inspiré par cette connexion et basé sur le livre « Models and games » par Väänänen, avec d’explorations supplémentaires en théorie descriptive des ensembles, les grands cardinaux et la décidabilité.

Preuves et programmes : Outils classiques

8 ECTS, semestre 2

Prérequis
Validationexamen
EnseignantAntonio Bucciarelli et Claudia Faggian
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é à quelques développements plus récents.

Quantification du second-ordre et points-fixes en logique

8 ECTS, semestre 2

Prérequissuivre le cours preuves-programmes : outils classiques en parallèle de ce cours constituera un complément judicieux.
Validationexamen
EnseignantAlexis Saurin et Thomas Colcombet
Horaires hebdomadaires 4 h CM

Syllabus

Ce cours étudiera sous différents aspects la notion de second-ordre en logique et étudiera les logiques à points-fixes. On abordera notamment différentes applications informatiques de ces formalismes logiques à l'étude des langages formels sur les mots et les arbres et à l'étude des langages de programmation.

Calculabilités : Outils classiques

8 ECTS, semestre 2

Prérequis
ValidationCC+examen
EnseignantLudovic Patey et Julien Cervelle
Horaires hebdomadaires 4 h CM

Syllabus

Ce cours est une continuation naturelle du cours "Calculabilité et incomplétude" du premier semestre. Les travaux de Godel, Church, Turing et d'autres, sur la définition formelle d'ensemble calculable, ont posés les bases sur lesquelles allait s'échafauder l'étude des degrés d'insolubilité : un important corpus de connaissances permettant de classer et comprendre l'univers des objets incalculables. Nous mèneront durant ce cours une étude détaillée de cet univers.

La calculabilité a aussi obtenu des succès majeurs en fournissant un cadre formel pour l'étude de certaines questions épistémologiques. Nous en verrons un exemple avec l'étude de l'aléatoire algorithmique. Nous verrons comment utiliser la calculabilité pour étudier avec une approche mathématique la question informelle de ce qu'est une suite de bits ``aléatoire''.

La deuxième partie du cours traite de la complexité de Kolmogorov. On donnera les définitions et les propriétés élémentaires. Nous verrons comment on utilise la complexité algorithmique dans les preuves de complexité. Nous étudierons les objets aléatoires finis et infinis.

Algèbre homotopique et catégories supérieures

4 ECTS, semestre 2

PrérequisConnaissances de base en théorie des catégories
ValidationCC+examen
EnseignantPierre-Louis Curien
Horaires hebdomadaires 2 h CM

Syllabus

La théorie de l'homotopie, ou l'étude des espaces topologiques à déformation près, a fait surgir une branche de l'algèbre appelée algèbre homotopique, où sont développés les outils pour la description de structures où les lois telles que l'associativité ne sont plus vérifiées exactement comme en algèbre classique, mais à homotopie près, ces homotopies étant elles-mêmes sujettes à des cohérences, et ainsi de suite.

La théorie de l'homotopie a aussi une dimension logique, avec l'interprétation de la notion de type comme espace, de preuve d'égalité comme chemin dans un espace et de preuve d'égalité de preuves d'égalité comme une homotopie entre chemins. Ces liens ont donné naissance à la théorie homotopique des types. La notion de fibration, qui joue un rôle essentiel en théorie de l'homotopie, est intimement liée à la notion de substitution en théorie des types dépendants.

Le cours, qui fera suite au cours de théorie des catégories du premier semestre, mais peut être suivi par des étudiants ayant déjà acquis ces bases par ailleurs, introduira les notions importantes sous-jacentes au domaine: les catégories enrichies, les catégories de modèles, et différentes façons de définir les catégories supérieures, notamment via les ensembles simpliciaux. Seront abordés aussi des sujets connexes comme les opérades et les ∞-opérades, eux aussi issus de la topologie. Le cours s'appuiera en partie sur plusieurs ouvrages parus dans les années récentes (Categorical homotopy theory d' Emily Riehl, The homotopy theory of (∞, 1)-categories de Julia Bergner, From categories to homotopy theory de Birgit Richter, Higher categories and homotopical algebra de Denis-Charles Cisinski, Simplicial methods for higher categories de Simona Paoli, qui offrent autant de lectures d'approfondissement pour les étudiantes et étudiants intéressés), avec une attention portée aux liens avec la théorie homotopique des types.

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 2021

Pour toutes les autres candidatures

Les étudiants doivent déposer leur dossier et pièces justificatives sur le site de l'université du 3 mai au 15 juillet 2022. Une seconde phase de candidatures a lieu du 23 août au 15 septembre.

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 2022 : 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 3 mai au 15 juillet 2022 : dépôt de dossier d'inscription sur le site E-candidat.
  • Du 23 août au 15 septembre 2022 : dépôt de dossier d'inscription sur le site E-candidat pour un examen de votre candidature à la session de septembre.
  • début septembre 2022 : cours préliminaire facultatif.
  • mi-septembre 2022 : 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