Admission

Requirements : first year master's, with a major in mathematics, computer science or logic – or equivalent

Application file : Registration will open on May 1st, 2020.

Careers

The LMFI naturally leads to pursuing a PhD, either in mathematical logic or in (fundamental) computer science.http://pubmaster.math.univ-paris-diderot.fr/admin/root:annee:m2-lmfi/preview

Curriculum

One term of core classes, one term of advanced classes and a research internship.

Curriculum

LMFI consists of:

  • During the first term:
    • an intensive introductory class in logic (30h), optional;
    • four core classes (three 48h classes, one 84h class, 20 ECTS);
    • core classes exercices session (36h each, 8 ECTS each).
  • During the second term:
    • a choice of eight advanced classes (48h each);
    • a choice of three ouverture classes (24h chacun);
    • an research internship (Master's thesis), supervised by an academic.

Classes may be taught in English, if so requested by the students.

Introduction to research

The Master's internship can take place, subject to approval by the Master's directors, either:

Studying abroad

contact: Tomás Ibarlucía

Erasmus+ programme

LMFI is in partnership with Logic Groups at several European universities (Turin, Münster, Pisa, Freiburg, Florence...). With the Erasmus+ exchange programme, students and teachers from partner universities can participate in some of the LMFI activities, and students and teachers from LMFI can participate in some of the activities of partner universities. The list of all universities which have a partnership with Université Paris Diderot is available here.

Erasmus+ incoming: If you are a Master's student at one of the partner universities, you can apply for a study abroad period at LMFI (1st term, 2nd term or both). The application procedure and deadlines depend on your university (ask a logic teacher or the person responsible for international exchanges at your home university).

Erasmus+ outgoing: If you are an M1 student at Paris Diderot or an LMFI student, you can apply for a study abroad period at one of the partner universities (4 to 10 months). For more details (application procedure and deadlines, the best partner destinations to study logic, etc.), ask Tomás Ibarlucía.

Research internships (Master's thesis)

Incoming: If you are a Master's student at any foreign university and you wish to do a research internship (Master's thesis) in mathematical logic or theoretical computer science at Université Paris Diderot, then you should contact Boban Velickovic and Antonio Bucciarelli.

Outgoing: If you are an LMFI student and you wish to write your Master's thesis (stage) under the supervision of a researcher at some foreign university (or under the joint supervision of a researcher in Paris and a foreign researcher), then you should contact Tomás Ibarlucía](mailto:ibarlucia@math.univ-paris-diderot.fr).

24/25 Calendar

  • September 2 to September 13 2024: intensive introductory class;
  • September 16 to December 6 2024: core classes;
  • December 16 to 20, 2024: first term exams;
  • January 6 to March 28, 2025: advanced and ouverture classes;
  • April 7 to 11, 2025: second term exams;
  • from April 14, up to September 29, 2025: introduction to research intership/dissertation

The first term schedule can be found here.

Program requirements

To obtain the LMFI degree, a 2nd year Master's degree, students must obtain 60 ECTS distributed as follows:

  • the four core classes (20 ECTS);
  • two advanced classes (8 ECTS each);
  • 8 ouverture ECTS obtained either:
    • by taking two ouverture classes (4 ECTS each);
    • by taking a third advanced class (8 ECTS);
  • the internship/dissertation (16 ECTS).

Ouverture classes can be chosen form the LMFI ouverture classes, or, subject to approval by the Master's directors, among the classes of others 2nd years Master's, for example in the Fundamental Mathematics master's or the MPRI (Master Parisien de recherche en informatique).

Courses

1st term

Preliminary Logic Course

0 ECTS, semestre 1

Requirements
Program requirementssans
TeacherPatrick Simonetta et Pierre Letouzey
Weekly hours 18 h CM

Syllabus

  • Propositional calculus: truth tables, tautologies, normal forms, compactness.
  • Predicate calculus: first-order languages, terms, formulas, models; satisfaction of a formula in a model; substructures; isomorphisms; elementary equivalence.
  • Set theory: axioms of Zermelo-Frænkel; cardinals; Cantor and Cantor-Bernstein theorems; finite sets, countable sets.
  • Introduction to programming: introduction to Ocaml functional programming; connection to lambda-calculus, recursivity, ML typing; common data structures (Boolean, integers, lists, options, trees, etc.).

Model Theory

4 ECTS, semestre 1

Requirements
Program requirementsexamen
TeacherTomas Ibarlucia
Weekly hours 2 h CM , 2 h TD

Syllabus

  • 1st-order languages, structures, theories
  • Ultraproducts, compactness.
  • Elementary extensions, Lowenheim-Skolem theorems, elementary chains.
  • Preservation theorems.
  • Back-and-forth arguments.
  • Quantifier elimination, model completeness
  • The space of types.
  • (If time allows it) Realized and omitted types, atomic models.

Set Theory

4 ECTS, semestre 1

Requirements
Program requirementsexamen
TeacherAlessandro Vignati
Weekly hours 2 h CM , 2 h TD

Syllabus

  • Axioms of ZF
  • Ordinals, cardinals, transfinite recursion
  • Ordinal and cardinal arithmetic
  • The Axiom of Choice and equivalents, filters and ultrafilters
  • Cofinality, regular/singular cardinals, König's theorem
  • Stationary and club sets, Fodor's lemma
  • Absoluteness and reflection theorems
  • The constructible universe

Proof Theory

4 ECTS, semestre 1

Requirements
Program requirementsexamen
TeacherThierry Joly
Weekly hours 2.0 h CM , 2.0 h TD

Syllabus

  • Completeness theorem of the LK sequent calculus with equality by Henkin's witnesses.
  • Sequent calculus: cut elimination of and median sequent theorem in LK. Herbrand's theorem. LJ sub-calculation: intuitionist logic and its BHK interpretation. Properties of the sub-formula and existential witnesses in LJ.
  • Natural deduction: NK and NJ systems. Cut elimination in NJ. Properties of the sub-formula and existential witnesses in NJ, then in HA (intuitionist arithmetic).
  • Lambda-calculus: Confluence and standardization properties. Representation of recursive functions. T system. Curry-Howard correspondence. Realizability, strong standardization and program correctness.

Computability and Incompleteness

8 ECTS, semestre 1

Requirements
Program requirementsexamen
TeacherArnaud Durand
Weekly hours 4 h CM , 2 h TD

Syllabus

  • Computability: recursive functions and functions computable by machines; logical characterization of computable functions; s-m-n theorem and fixed point theorems; the concept of reduction and undecidable problems.
  • Introduction to complexity: time and space complexity classes, hierarchy theorems, reductions, completeness, Boolean circuits, introduction to algebraic complexity.
  • Formal arithmetic: Peano axioms and weak subsystems; arithmetization of logic; undecidability theorems; Gödel's incompleteness theorems.

Category Theory

4 ECTS, semestre 1

Requirements
Program requirementsExamen
TeacherFrancois Metayer
Weekly hours 2 h CM

Syllabus

The course presents the fundamental concepts of category theory, accompanied by numerous examples. The main goal is to pave the way towards the modern applications of category theory in logic, theoretical computer science and homotopy theory.

Functional programming and formal proofs in Coq

8 ECTS, semestre 1

Requirements
Program requirementsprojet
TeacherPierre Letouzey
Weekly hours 2 h CM , 2 h TP

Syllabus

One half of this module will consist of course work, the other half will consist of practical work on a machine. The course will finish with a project to be carried out in Coq. The first part of this course is a prerequisite for the Homotopy Type Theory course.

2nd term

Model Theory: classical tools

8 ECTS, semestre 2

RequirementsBesides the notions and results of the first semester course, a general mathematical background (at Bachelor's level) will be useful to understand some examples and applications.
Program requirementsCC+examen
TeacherSylvy Anscombe
Weekly hours 4.0 h CM

Syllabus

This course is a natural continuation of the first semester Model Theory course. It will seek to understand and classify the models of a given 1st order theory through the types that can be realized or omitted.

Model Theory: advanced topic (Continuous and Affine Logics)

8 ECTS, semestre 2

Requirements
Program requirementsCC+examen
TeacherTomas Ibarlucia
Weekly hours 4.0 h CM

Syllabus

Dans ce cours nous étudierons la théorie des modèles des structures métriques, telles que les espaces de Hilbert et de Banach, les algèbres de probabilité, les systèmes ergodiques ou les algèbres d'opérateurs. Celle-ci est basée sur le formalisme de la logique continue, une généralisation naturelle (à valeurs réelles) de la logique du première ordre classique. Nous étudierons également en détail un fragment distingué de la logique continue, appelé logique affine, et ses connexions toutes récentes avec la théorie de Choquet en analyse fonctionnelle.

Set Theory: classical tools

8 ECTS, semestre 2

Requirements
Program requirementsexamen
TeacherBoban Velickovic
Weekly hours 4 h CM

Syllabus

On 8 August 1900, at the Second International Congress of Mathematicians in Paris, David Hilbert set out a list of 23 mathematical problems which, in his opinion, should serve as a guide for future research in the new century. The first problem in this list, Cantor's continuum hypothesis, was solved in two stages: by Gödel (1938) who constructed an internal model of the generalized continuum hypothesis, and by Paul Cohen (1963), who invented a model construction for the negation of Cantor's hypothesis. This course will mainly cover the two model constructions of set theory introduced by Gödel and Cohen.

Set Theory: advanced topic (Large cardinals))

8 ECTS, semestre 2

Requirements
Program requirementsCC+examen
TeacherBoban Velikovic
Weekly hours 4.0 h CM

Syllabus

Large cardinal axioms postulate the existence of cardinals with a given degree of transcendence over smaller cardinals and provide a superstructure for the analysis of strong mathematical statements. The investigation of these axioms is indeed a mainstream of modern set theory. For instance, they play a crucial role in the study of definable sets of reals and their regularity properties such as Lebesgue measurability. Although formulated at various stages in the development of set theory and with different motivation, these hypotheses were found to form a linear hierarchy reaching up to the inconsistency. All known set-theoretic propositions can be gauged in this hierarchy in terms of their consistency strength, and the emerging structure of implications provides a remarkably rich, detailed and coherent picture of the strongest propositions of mathematics as embedded in set theory.

Proofs and programs: advanced topic (Linear Logic and Quantitative Semantics)

8 ECTS, semestre 2

Requirements
Program requirementsCC+examen
TeacherClaudia Faggian et Gabriele Vanoni
Weekly hours 4.0 h CM , 0.0 h TD

Syllabus

The Curry-Howard correspondence highlights deep links between proofs and programs. Linear logic has profoundly renewed this connection between the formal semantics of programming languages on one hand and proof theory on the other, by bringing attention to the dynamics of programs (how the computation is performed) and on the use of resources. An outcome of this attention to resources are quantitative approaches to calculi, to types and to the semantics. Quantitative systems are able to provide information such as the cost of computation, and are crucial to express paradigms of computation which are intrinsically quantitative, such as probabilistic, differential or quantum computation.

Computability: advanced topic (Advanced Complexity)

8 ECTS, semestre 2

Requirements
Program requirementsCC+examen
TeacherHervé Fournier et Guillaume Malod
Weekly hours 4.0 h CM

Syllabus

Nous aborderons différents thèmes de complexité. En complexité booléenne, nous parlerons en particulier de complexité de comptage et de complexité de communication. Nous étudierons aussi la complexité algébrique, sur laquelle s'appuient certains efforts récents pour résoudre le problème P vs. NP. En plus d'une présentation générale, nous explorerons des régimes calculatoires restreints, notamment les calculs non-commutatifs, et présenteront certaines bornes inférieures et les techniques de rang qui permettent de les obtenir.

Model-checking Finite Structures

4 ECTS, semestre 2

RequirementsFirst semester computability and incompleteness; the second semester course on model theory can be a plus.
Program requirementsCC
TeacherSylvain Schmitz
Weekly hours 2.0 h CM

Syllabus

The course is dedicated to the model-checking problem over finite structures, with a particular focus on algorithmic meta-theorems, the main highlight of the course being Courcelle's Theorem.

A number of topics are touched upon through this lens, including some basics in complexity theory, circuit complexity, parameterised complexity, monadic second-order logic, tree languages, logical transductions, structural graph theory, etc.

Admission

(check for updates in the fernch version of the webpage!)

Candidates must have a 1st year master's degree (M1), or an equivalent degree, with a major in mathematics, computer science or logic.

Application of foreign students (oustide EU and Switzerland)

In order to make the application process easier for international students, the University of Paris Diderot follows the Campus France procedure. Foreign students should find all relevant information on the Campus France website. Foreign students from countries involved in the "Étude en France" procedure should register on that platform before March 2019.

For all other applications

Students must apply on the university website from Mai the 1st to July 15.

Scholarships

There are possibilities of scholarships for prospective M1 or M2 students, and particularly for foreigners:

Important deadlines:

  • February 6th 2025: deadline for foreign students who apply via the "Étude en France" procedure, see the Campus France website for details. This does not apply to students already enrolled in a university establishment in France or European Union citizens.
  • May-June 2025: application on the E-candidate website.
  • August 23th to September 15th, 2022: application on the E-candidate website, for a review in the September session.
  • early September 2025: optional introductory class.
  • mid September 2025: start of the core classes.

Careers

The LMFI naturally leads to pursuing a PhD, either in mathematical logic or in (fundamental) computer science. Phd's in computer science can also be pursued in a compagny or a public research institute (INRIA, CEA, ONERA, etc.). In recent years, more than half of the students that obtained the LMFI Master's degree have continued with a PhD thesis.

The main career prospects after a PhD thesis are in research in a broad sense:

  • in academia (French or foreign) or public research institutes (CNRS, INRIA, CEA, ONERA, etc.);
  • in private sector research and development departments (EDF, France Telecom, Siemens, EADS, etc.). Research and development departments are particularly interested in recruiting people with strong mathematical, logical and computer skills, allowing them to supervise engineers in software certification, program and protocol verification and more generally in cyber security. In some cases, recruitment may take place directly after the Master's degree.

Practical informations