Le Laboratoire Méthodes Formelles (LMF) est né le 1er janvier 2021 de la volonté politique de ses tutelles - Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria et CentraleSupélec - de créer un pôle ciblé sur les méthodes formelles. Le LMF est formé du Laboratoire Spécification et Vérification (LSV, ENS Paris-Saclay, CNRS, Inria) et de l’équipe Vals du Laboratoire de Recherche en Informatique (LRI, Université Paris-Saclay, CNRS, Inria, CentraleSupélec) soit une centaine de personnes.

Son ambition est d’éclairer le « monde numérique » grâce à la logique mathématique en utilisant les méthodes formelles comme outil d’analyse, de modélisation et de raisonnement pour les programmes informatiques, les protocoles de sécurité, etc. Il s'appuie sur des paradigmes de calcul des plus classiques aux plus novateurs comme l’informatique quantique.

Le LMF est structuré en pôles : son cœur de métier en comporte deux, « Preuves » et « Modèles » ; le troisième, « Interactions », est une ouverture à d’autres domaines tels que l’IA et la biologie.

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.

Apr 29 14:00 ₂₀₂₅

Abstract:

Regular word grammars are context-free grammars having restricted rules, that define all recognizable languages of words. This paper generalizes regular grammars from words to certain classes of graphs, by defining regular grammars for unordered unranked trees and graphs of tree-width 2 at most. The qualifier ``regular'' is justified because these grammars define precisely the recognizable (equivalently, CMSO-definable) sets of the respective graph classes. The proof of equivalence between regular and recognizable sets of graphs relies on the effective construction of a recognizer algebra of size doubly-exponential in the size of the grammar. This sets a 2EXPTIME upper bound on the (EXPTIME-hard) problem of inclusion of a context-free language in a regular language, for graphs of tree-width 2 at most. A further syntactic restriction of regular grammars suffices to capture precisely the MSO-definable sets of graphs of tree-width 2 at most, i.e., the sets defined by CMSO formulae without cardinality constraints. Moreover, we show that MSO-definability coincides with recognizability by algebras having an aperiodic parallel composition semigroup, for each class of graphs defined by a bound on the tree-width.

This is joint work with Marius Bozga (Verimag) and Florian Zuleger (TU Wien).

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.

Chaque année, l'Académie des sciences remet près de quatre-vingt prix couvrant l'ensemble des domaines scientifiques, aussi bien fondamentaux qu'appliqués. Lors de la cérémonie de remise de prix du 26 novembre 2024, Gilles Dowek a reçu la Médaille d'histoire des sciences et d'épistémologie.

Gilles Dowek explore de nouvelles questions philosophiques posées par le développement de l'informatique. Ces questions portent sur le rôle du calcul dans la définition de la vérité mathématique, sur les rapports entre la thèse de Church-Turing et celle de Galilée, selon laquelle l'Univers est écrit en langue mathématique, sur la notion de langage formel et son lien à l'écriture et sur la construction d'une éthique de l'informatique. — Citation du prix

La médaille d’Histoire des sciences et d’épistémologie récompense une ou un scientifique en pleine activité de toute nationalité travaillant dans un laboratoire français de recherche public ou privé ayant contribué par des résultats particulièrement prometteurs au développement de sa discipline, sans restriction sur la nature fondamentale ou appliquée de ses recherches.

Crédit photo : © Académie des sciences – Mathieu Baumer