The Laboratoire Méthodes Formelles (LMF) was founded on 1 January 2021 as a joint research centre of University Paris-Saclay, CNRS, ENS Paris-Saclay, Inria, and CentraleSupélec with a main focus on formal methods. The new laboratory combines the expertise of about 100 members from the former Laboratoire Spécification et Vérification (LSV) and the VALS team of Laboratoire de Recherche en Informatique (LRI).

In our mission to enlighten the digital world through Mathematical Logic, we rely on formal methods as a tool to analyse, model, and reason about computing systems, such as computer programs, security protocols, and hardware designs. Our research targets a wide range of computational paradigms, from classical to emerging ones such as biological and quantum computing.

LMF is structured around three hubs: Proofs and Models, which lie at the heart of our historical background, and Interactions, that is aimed at fostering cross-fertilisation between formal methods and other domains in computing science and beyond.

Quatre postes d'enseignant·e·s-chercheur·e·s avec affectation au LMF ouvrent en 2025 :

• Un poste de professeur·e à la Faculté des Sciences, Université Paris-Saclay
• Un poste de professeur·e à l'ENS Paris-Saclay
• Un poste de maître·sse de conférences à la Faculté des Sciences, Université Paris-Saclay
• Un poste de maître·sse de conférences à Polytech, Université Paris-Saclay

Learn Programming with OCaml is a new book by Sylvain Conchon and Jean-Christophe Filliâtre. This is an English translation (by Urmila Nair) of the French edition Apprendre à programmer avec OCaml.

The book is available as a PDF file, under the CC-BY-SA license. The source code for the various programs contained in the book is available for download, under the same license.

The book is structured in two parts. The first part is a tutorial-like introduction to OCaml through 14 small programs, covering many aspects of the language. The second part focuses on fundamental algorithmic concepts, with data structures and algorithms implemented in OCaml.

Combining computational theories

Feb 3 14:30 ₂₀₂₅

Monday 3 February 2025 at 14h30
ENS Paris-Saclay, Room 1Z14

Abstract. Proof checkers and proof assistants are used to formalize mathematical theorems and verify software, notably critical systems such as medical, industrial and transport systems. The diversity of proof systems raises the question of their interoperability: how can proofs be rechecked and reused across systems? Logical frameworks such as the λΠ-calculus modulo theory provide a common formalism in which various logical systems and mathematical theories can be expressed. The proof transformation tools within the λΠ-calculus modulo theory allow proofs to be translated from one logical system another. In a similar way to logical frameworks, theories combining several theories provide a common language between theories. The main focus of this manuscript is the study of the definition and properties of these theories, specifically in the context of computational theories, that is whose definition relies on rewriting. Read more...

We are delighted to announce that two researchers with strong ties to our laboratory have won the Ackermann Award 2024:

🌟 Gaëtan Douéneau-Tabot

A former student at ENS Paris-Saclay, Gaëtan was recognised for his thesis, Optimization of String Transducers, supervised by Olivier Carton (IRIF, Université Paris-Cité) and Emmanuel Filiot (Université Libre de Bruxelles).

🌟 Aliaume Lopez

Aliaume completed a joint PhD between LMF and IRIF (Université Paris-Cité). His award-winning thesis, First Order Preservation Theorems in Finite Model Theory: Locality, Topology, and Limit Constructions, was supervised by Jean Goubault-Larrecq (LMF) and Sylvain Schmitz (IRIF, Université Paris-Cité).

Read more...

Aliaume Lopez received the 2024 E. W. Beth Dissertation Prize for his thesis First Order Preservation Theorems in Finite Model Theory : Locality, Topology, and Limit Constructions.

The prize, named in honor of the Dutch mathematician Evert Willem Beth, was established in 1998 by the Association for Logic, Language, and Information (FoLLI) and is awarded annually for outstanding dissertations in the fields of Logic, Language, and Information.

Aliaume prepared his thesis under the joint supervision of Jean Goubault-Larrecq at LSV, then LMF, and of Sylvain Schmitz at IRIF.

Each year, the French Academy of Sciences awards nearly eighty prizes covering the entire specrum of fundamental and applied sciences. At the award ceremony of 26 November, 2024, Gilles Dowek was bestowed with the Medal for Contributions to the History and Philosophy of Science.

Gilles Dowek explores new philosophical questions raised by the development of computer science. These questions address the role of computation in defining mathematical truth, the relationship between the Church-Turing thesis and Galileo's principle that the Universe is written in the language of mathematics, the concept of formal languages and their connection to writing, and the construction of an ethics of computer science.

— Award citation

The Medal for Contributions to the History and Philosophy of Science is awarded to an active scientist of any nationality working in a French public or private research laboratory who has contributed particularly promising results to the development of their discipline, without restriction on the fundamental or applied nature of their research.

Photo credit: © Académie des sciences – Mathieu Baumer