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.

Patricia Bouyer (LMF, CNRS), B Srivathsan (CMI and ReLaX, India) and Vaishnavi Vishwanath (CMI, India) received the Best ETAPS Paper Award in 2025, which is given to the best theoretical paper at ETAPS, the International Joint Conferences on Theory and Practice of Software. Read more...

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.

A New Scientist column  entitled "Where does time actually come from?" discusses the recent contribution by Pablo Arrighi and Gilles Dowek from LMF and Amélia Durbec from IEMN, to the somewhat fundamental questions about the nature of Time.

Since the laws of Physics are time-reversible, what makes the difference between past and future? Entropy may increase, but how come it was low to begin with? And by-the-way, what happened even before it was at its lowest? And what if... working with toy model graph dynamics, could suggest simple CompSci answers to big Physics questions?

Mickaël Laurent, ancien doctorant du LMF et de l'IRIF, encadré par Giuseppe Castagna et Kim Nguyễn, a reçu le prix de thèse du GdR Génie de la Programmation et du Logiciel, décerné le 19 juin lors des journées nationales du GdR.

Sa thèse est intitulée Inférence de types polymorphes pour des langages dynamiques : reconstruction de types pour des systèmes combinant polymorphisme paramétrique, surcharge et sous-typage”. Félicitations à Mickaël pour son excellent travail !

(photo avec l'autorisation des personnes, de gauche à droite Anouck Chan, première accessit, Pascal Poizat, co-président du jury et Mickaël)

Plus d'informations sur le site du GdR.

Synthesis for Games of Imperfect Information under Full-Information Protocols

Jul 7 14:00 ₂₀₂₅

Lundi 7 juillet 2025 à 14h00
ENS Paris-Saclay, Salle 1B36 et visio

Résumé : Différents modèles peuvent être utilisés pour représenter des programmes, pour vérifier s’ils sont corrects, ou mieux pour en synthétiser à partir d’une spécification. Nous modélisons ici un programme par un joueur affrontant un environnement. Construire un programme correct revient alors à synthétiser une stratégie gagnante dans ce jeu, c’est à dire un comportement qui assure de vérifier la condition de victoire quel que soit le comportement de l’environnement.

Nous introduisons un nouveau type de jeu dans lesquels le joueur obtient une information imparfaite en communiquant avec des observateurs passifs, via un full-information protocol. Contrairement au modèle classique on peut obtenir en un instant une quantité non bornée d'information.

Nous proposons une méthode pour synthétiser des stratégies pures et randomisées dans ces jeux, applicable dès qu'un morphisme information-commutant peut être construit.

Read more...

Aspects of Category Theory in Proof Assistants

Jul 7 14:00 ₂₀₂₅

Monday 7 July 2025 at 14h00
ENS Paris-Saclay, Room 1B26

Abstract: While the use of proof assistants in mathematical research has yet to become the norm, an increasing number of results have been formalized. The prevalence of category theory in recent mathematical research indicates the need for its formalization in proof assistants. However, category theory is challenging to formalize for reasons we will explore.

The first difficulty is due to the fact that proposition equality in dependently typed theories as a structure that interacts in a complicated way with categories formalised inside those theories. We describe those challenges, and propose some solutions we explored to this problem.

Read more...