### 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.

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.

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

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

- Director of studies : Antonio Bucciarelli, Boban Velickovic

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).

- an
- 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.

- a choice of eight

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

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

- in one of the two host departments: the Institut de mathématiques de Jussieu - Paris Rive Gauche (and more particulary its Logic team) or the Institut de recherche en informatique fondamentale;
- in one the of the many Parisian universities where research in logic is conducted: the École Normale Supérieure, the Université Paris-Saclay...
- in other French universities: the Université Claude Bernard, in Lyon, the Université Aix-Marseille...
- in other European universities : Torino, Pisa, Münster, Freiburg, Düsseldorf, Florence...

contact: Tomás Ibarlucía

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.

*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).

**August 29 to September 9 2022**: intensive introductory class;**September 12 to December 2 2022**: core classes;**December 12 to 16, 2022**: first term exams;**January 3 to March 25, 2023**: advanced and ouverture classes;**April 3 to 7, 2023**: second term exams;**from April 10, up to September 29, 2023**: introduction to research intership/dissertation

The first term schedule can be found here.

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).

0 ECTS, semestre 1

Requirements | |

Program requirements | sans |

Teacher | Patrick Simonetta et Pierre Letouzey |

Weekly hours | 18 h CM |

- 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.).

4 ECTS, semestre 1

Requirements | |

Program requirements | examen |

Teacher | Tomas Ibarlucia |

Weekly hours | 2 h CM , 2 h TD |

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

4 ECTS, semestre 1

Requirements | |

Program requirements | examen |

Teacher | Alessandro Vignati |

Weekly hours | 2 h CM , 2 h TD |

- 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

4 ECTS, semestre 1

Requirements | |

Program requirements | examen |

Teacher | Thierry Joly |

Weekly hours | 2 h CM , 2 h TD |

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

8 ECTS, semestre 1

Requirements | |

Program requirements | examen |

Teacher | Arnaud Durand |

Weekly hours | 4 h CM , 2 h TD |

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

4 ECTS, semestre 1

Requirements | |

Program requirements | Examen |

Teacher | Francois Metayer |

Weekly hours | 2 h CM |

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.

8 ECTS, semestre 1

Requirements | |

Program requirements | projet |

Teacher | Pierre Letouzey |

Weekly hours | 2 h CM , 2 h TP |

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.

6 ECTS, semestre

Requirements | |

Program requirements | |

Teacher |

8 ECTS, semestre 2

Requirements | Besides 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 requirements | examen |

Teacher | Elisabeth Bouscaren |

Weekly hours | 4 h CM |

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.

8 ECTS, semestre 2

Requirements | |

Program requirements | examen |

Teacher | Tamara Servi |

Weekly hours | 4 h CM |

In model-theoretic terms, an expansion M of the real ordered field is o-minimal if all M-definable subsets of the reals have finitely many connected components. This can also be formulated in purely geometric terms, as a property of a collection of real sets, stable under the boolean set-operations, Cartesian products and linear projections. The sets definable in an o-minimal structure share many topological tameness properties with real algebraic and real analytic sets (good dimension theory, uniform finiteness, stratification), which makes o-minimal geometry relevant to problems in Diophantine and arithmetic geometry, non-oscillatory dynamical systems and asymptotic analysis. I will give an overview of the main results about o-minimal structures and then I will concentrate on illustrating the main methods for proving that a collection of real functions generates an o-minimal structure. There are essentially no prerequisites for this course, other than the basic undergraduate notions of algebra and analysis: the model-theoretic background needed is minimal and self-contained references will be provided to those who might need them.

8 ECTS, semestre 2

Requirements | |

Program requirements | examen |

Teacher | Boban Velickovic |

Weekly hours | 4 h CM |

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.

8 ECTS, semestre 2

Requirements | |

Program requirements | Examen |

Teacher | Mirna Dzamonja |

Weekly hours | 4 h CM |

The module will explore the ways that logic interact with the theory of games. Some examples where game theory enters set theory are strategic closure and determinacy, for model theory Ehrenfeucht-Fraïssé games, for descriptive complexity the pebble game, for automata theory certain decision arguments. Jouko Väänänen states that there are essentially three kinds of games in logic, and that there are essentially connected, forming a « strategic balance of logic ». We shall explore that balance. Lectures will be based on « Models and games » by Jouko Väänänen, with some additional explorations into descriptive set theory, large cardinals and decidability.

8 ECTS, semestre 2

Requirements | |

Program requirements | examen |

Teacher | Antonio Bucciarelli and Claudia Faggian |

Weekly hours | 4 h CM |

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 programs, 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 some more recent developments.

6 ECTS, semestre

Requirements | |

Program requirements | |

Teacher |

4 ECTS, semestre 2

Requirements | Basic knowledge in category theory |

Program requirements | CC+examen |

Teacher | Pierre-Louis Curien |

Weekly hours | 2 h CM |

Homotopy theory, which is devoted to the study of spaces up to deformation, has given rise to a branch of algebra called homotopical algebra, in which tools are developed for dealing with structures in which laws like associativity do not hold exactly like in classical algebra, but up to homotopy, these homotopies being themselves subject to coherences, etc.

Homotopy theory has also a logical side, in which types, proofs of equality, and proofs of equality of proofs of equality are interpreted as spaces, paths, and homotopies between paths, respectively. The notion of fibration, that plays an essential rôle in homotopy theory, is tightly related with substitution in dependent type theory. This interplay has led to a new version of type theory called homotopy type theory.

The course is a follow-up of that on category theory taught in the first semester, but can be followed by students who have already some basic background in category theory. We shall introduce the important notions underlying the subject: enriched categories, model categories, as well as different approaches to the definition of higher catégories, notably via simplicial sets. We shall also hint at connected subjects such as operads and ∞-operads, that also have arisen from topology. The lectures will partly follow the flow of exposition found in recent books (Categorical homotopy theory by Emily Riehl, The homotopy theory of (∞, 1)-categories by Julia Bergner, From categories to homotopy theory by Birgit Richter, Higher categories and homotopical algebra by Denis-Charles Cisinski, Simplicial methods for higher categories by Simona Paoli, which all offer opportunities to the interested students for learning more), with an eye on the links with homotopy type theory.

4 ECTS, semestre 2

Requirements | |

Program requirements | CC+examen |

Teacher | Brice Halimi |

Weekly hours | 2 h CM |

4 ECTS, semestre 2

Requirements | |

Program requirements | CC+examen |

Teacher | Lorenzo Tortora de Falco |

Around the middle of the eighties of the last century, when thanks to the Curry-Howard correspondence the field of research at the crossroads of theoretical computer science and demonstration theory was booming, Jean-Yves Girard introduced and studied denotational models of the system F. He then discovered a very simple model of F, the coherent spaces, which possess remarkable duality properties, and that the connectors of intuitionistic logic can be decomposed by means of more elementary operations in this model. Moreover, it turns out that this decomposition can be internalized through new logical connectors: this is how Linear Logic appears, as the underlying structure of "logic" in general, and of computational processes. Linear Logic is a powerful tool to analyze and control the use of resources in logic and computer science. Its nature as the underlying structure of logic has led researchers to develop techniques, approaches and methods that have been applied in many other fields (sequentiality theory, Scott semantics, lambda-calculus, game semantics, analysis of classical logic and its computational content, implicit complexity, verification, etc.).

The course will present some fundamental tools of proof theory of linear logic. They will be introduced on the basis of the questions that led to their development and we will try to highlight the perspectives opened up by their properties.

4 ECTS, semestre 2

Requirements | |

Program requirements | CC+examen |

Teacher | Camille Bourgaux, Michaël Thomazo |

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

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.

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

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

- List of scholarship programs on Campus France;
- PGSM program of the Fondation des Sciences Mathématiques de Paris.

**March 2022**: 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 3rd to July 15th, 2022**: 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**: optional introductory class.**mid September**: start of the core classes.

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.