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.

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: Tamara Servi

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 Tamara Servi.

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 Christine Tasson.

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 Tamara Servi.

19/20 Calendar

  • September 2nd to 13th, 2019: intensive introductory class;
  • September 16th to December 6th, 2019: core classes;
  • December 16th to 20th, 2019: first term exams;
  • January 6th to March 27th, 2020: advanced and ouverture classes;
  • April 20th to 24th, 2020: second term exams;
  • from April 15th, up to September 30th, 2020: 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

The preliminary course will take place from September 2 to 13.

  • 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
TeacherTomás Ibarlucia
Weekly hours 2 h CM , 2 h TD

Syllabus

  • Ultraproducts, compactness.
  • Elementary extensions, Lowenheim-Skolem theorems.
  • Diagram method, preservation theorems.
  • Back-and-forth arguments, elimination of quantifiers.
  • The space of types, omitting types theorem, kappa-saturated models, atomic models.
  • Omega-categorical theories, Ryll-Nardzewski's theorem. Decidability of some axiomatic theories.

Set Theory

4 ECTS, semestre 1

Requirements
Program requirementsexamen
TeacherFrançois Le Maître
Weekly hours 2 h CM , 2 h TD

Syllabus

  • ordinals, transfinite recursion;
  • axiom of choice and equivalent statements;
  • arithmetic of infinite cardinals; cofinality, regular and singular cardinals, König's theorem;
  • von Neumann's hierarchy, reflection theorems;
  • filters and ultrafilters, stationary sets in $\omega_1$, Fodor's lemma;
  • well-founded relationships and Mostowski's collapse;
  • some elements of descriptive set theory.

Proof Theory

4 ECTS, semestre 1

Requirements
Program requirementsexamen
TeacherThierry Joly
Weekly hours 2 h CM , 2 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
TeacherPaul Rozière et Hervé Fournier
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.

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 requirementsexamen
TeacherTamara Servi
Weekly hours 4 h CM

Syllabus

This course is a natural continuation of the first semester Model Theory course: in the first semester course, given an L-structure M, you will identify all the L-statements which are true in M (i.e. the theory of M). Conversely, in this course, given a complete L-theory T, we will classify its models up to isomorphism.

Model theory of pseudo-finite fields

8 ECTS, semestre 2

RequirementsGalois theory. Rudiments of algebraic geometry and model theory would be welcome. Reminders will be done in class if necessary.
Program requirementsexamen
TeacherSilvain Rideau
Weekly hours 4 h CM

Syllabus

The asymptotic properties of finite fields, i.e. the properties that are true in every sufficiently large finite field, can be understood by looking at pseudo finite fields: the infinite models of set of statements that hold in every finite field. This class was defined by Ax and he gave an algebraic characterisation of it: they are exactly the perfect, pseudo- algebraically closed fields with exactly one extension of any given degree.

Pseudo finite structures have lately played an important role in the model theoretic study of certain questions in combinatorics, among others in results of Hrushovski in additive combinatorics. These results find some of their roots in the work of Chatzidakis, van den Dries and Macintyre that gave a precise description of sets definable in a pseudo-finite field by, among other things, exhibiting a pseudo-finite equivalent of of the counting measure. The goal of

The goal of this class will be to introduce the results of Ax and Chatzidakis-van den Dries-Macintyre as well as introduce the algebraic notions necessary to understand them. We will then consider questions related to geometric model theory like the study of definable groups, the imaginaries or classification questions.

Set Theory: classical tools

8 ECTS, semestre 2

Requirements
Program requirementsexamen
TeacherBoban Velikovic
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.

Descriptive Set Theory

8 ECTS, semestre 2

Requirements
Program requirementsExamen
TeacherDominique Lecomte
Weekly hours 4 h CM

Syllabus

In classical descriptive set theory, we are interested in sets appearing naturally in various topics in mathematics, in particular in functional analysis, harmonic analysis, dynamical systems and group theory. One of the goals is to study the topological complexity of these sets. For example, one can classify the Borel subsets of the real line by considering the number of steps necessary to construct them, starting from the open sets, and allowing countable unions and taking complements.

We work in Polish topological spaces, where Baire’s theorem is a powerful tool. We will first be interested in the Borel subsets of the Polish spaces, and we will see that the countable ordinals define a natural hierarchy among them. Then we will study the direct images of the Borel sets by the Borel maps (the analytic sets) and their complement (the co-analytic sets). In particular, we will provide a method allowing us to prove that some sets are co-analytic but not Borel.

We will finish this course with an introduction to effective descriptive set theory and its appli- cations. One of its very powerful tool is the Gandy-Harrington topology, and we will establish its properties allowing to use it to prove many dichotomy results. We will provide the details for at least three examples: the Hurewicz dichotomy, the Silver dichotomy and the Kechris-Solecki-Todorčević dichotomy. We will state some more recent examples, and give some details if time permits.

Proofs and programs: classical tools

8 ECTS, semestre 2

Requirements
Program requirementsexamen
TeacherChristine Tasson and Alexis Saurin
Weekly hours 4 h CM

Syllabus

Proof theory has undergone at least two major developments over the past century as a result of Gödel's incompleteness theorems. The first took place in the 1930s, immediately after the results on incompleteness, with the introduction and study of natural deduction and sequent calculus s by Gentzen and lambda-calculus by Church. Church then showed the undecidability of predicate calculus via lambda-calculus while introducing a universal computation model while Gentzen deduced the consistency of various logical systems as a corollary of cut elimination of breaks in sequent calculus.

The second stage took place in the 1960s with the gradual highlighting, through the Curry-Howard correspondence, of the profound links between proofs and programmes, from the correspondence between simply typed lambda-calculus and minimal propositional natural deduction to the various extensions of this correspondence to the second order, to classical logic and to the emergence of the notion of linearity in proof theory. Linear logic has profoundly renewed the links between the formal semantics of programming languages on one hand and proof theory on the other. Linear algebra is the third pole of this correspondence, focusing on the notion of computational resource.

The basic course covered the first step. This course will be devoted to the developments since the 1960s and will present the classical tools for the study of the Curry-Howard correspondence. After some review and additions to the basic course, the course will focus on two fundamental concepts, the second order and linearity, and their development, particularly in an algebraic context. In particular, the results of the course will be applied to the study of PCF, an idealized programming language.

Homotopy Type Theory

8 ECTS, semestre 2

RequirementsStudents following this class are expected to have attended the introduction to programming and to formal proofs in Coq, or equivalent background.
Program requirementsExamen
TeacherHugo Herbelin
Weekly hours 4 h CM

Syllabus

Basic Type Theory

  • Pure Type Systems
  • Martin-Löf's Type Theory
  • Calculus of Inductive Constructions
  • Proof/Program Correspondence
  • Proof Irrelevance
  • Inductive and Coinductive Types
  • Extensionality in Type Theory

Homotopy Type Theory

  • Type/Space and Equality/Path Correspondence
  • Homotopic Concepts in Type Theory (contractible spaces, h-levels, univalence, weak factorisation systems, fibrations, cofibrations)
  • Higher Inductive Types (spheres, quotients, truncations)
  • Axiom of Choice and Classical Reasoning In Homotopy Type Theory

Models

  • Categories with Families
  • Cubical Type Theory
  • Internal Translations
  • ω-groupoïdes
  • Kan complexes

Functional programming and formal proofs in COQ

8 ECTS, semestre 2

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

Syllabus

The course take place during the last 6 weeks of the 1st semester and the first 6 weeks of the 2nd semester.

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.

Descriptive Complexity: from discrete to continuous

8 ECTS, semestre 2

RequirementsIt will be assumed that students know the basics of calculability (especially primitive recursion) and complexity (P, NP).
Program requirementsexamen
TeacherArnaud Durand et Olivier Bournez
Weekly hours 4 h CM

Syllabus

The objective of the course is to present several points of view on complexity from logic, recursion theory or analysis. The common feature of these approaches is that they move away from the notion of the machine (and its associated measures such as time and space) in favour of a more descriptive view of the calculation. The course aims in particular to study logical formalisms in terms of their power of expression and to present multiple characterizations of the usual complexity classes.

These descriptive or implicit approaches to complexity have had important applications in database theory, programming languages and more recently in the analysis of differential equation systems, or in understanding the power of alternative computational models based on bioinformatics, or analog computation.

We will first aim to present results on classical complexity [8, 13], to extend to algebraic models such as Blum Shub and Smale's model [3, 2], to continuous space such as neural network/deep learning models [17], then to time and continuous space such as Shannon's model [16].

Blockchains, tokens and contracts

4 ECTS, semestre 2

Requirements
Program requirementsexamen
TeacherVincent Danos et Ilias Garnier
Weekly hours 2 h CM

Syllabus

The purpose of this course is to give an overview of computer science basics of blokchains (communication protocols, games) and examples of blockchain protocols used in cryptocurrencies and smart contracts.

History and Philosophy of Logic

4 ECTS, semestre 2

Requirements
Program requirementsCC+examen
TeacherBrice Halimi
Weekly hours 2 h CM

Syllabus

How is logic formal?

The course will be devoted to this question. In particular, we will examine three main reasons for declaring logic "formal": because it uses discursive resources that can be said to be formal (schematic); because it concerns forms (whose status is to be specified: "logical constants" for Russell, "forms derived from something in general" for Husserl, to mention two important examples); and because it aims at an independent validity of any particular content (logic as universal science).

These three main reasons are not necessarily compatible. Moreover, the examination of the question raised will of course imply taking into account the history of logic, and a reflection on the situation of logic between philosophy and mathematics. This will be an opportunity to examine the issue of "absolute generality", that is, the possibility of a theory covering absolutely everything in general.

Aim of the class: knowledge of the philosophical issues of the history of logic in the 20th century.

Admission

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 the 10th.

Scholarships

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

Important deadlines:

  • March 2020: 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 1st to July 10th, 2020: application on the E-candidate website.
  • August 24th to September 15th, 2020: application on the E-candidate website, for a review in the September session.
  • early September: optional introductory class.
  • mid September: 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