News

The CNRS blog Focus Sciences recently published an article, “The art of modelling complex computing systems”, featuring the work of the ANR project NARCO (Non-Aggregative Resource COmpositions). The project explores new logic-based methods to model and verify complex computing systems by capturing the real interactions—sharing, dependencies and coordination—between their components. At LMF, Mihaela Sighireanu leads the lab’s contribution, focusing on verification techniques grounded in extended separation logics. This approach promises more expressive yet automatable analyses of evolving systems. Learn more on the project presentation and discover its partners: LIG, VERIMAG and LORIA.

Le blog Focus Sciences du CNRS consacre un article, « L’art de modéliser des systèmes informatiques complexes », au projet ANR NARCO (Non-Aggregative Resource COmpositions). Ce projet développe de nouvelles approches logiques pour modéliser et vérifier des systèmes informatiques complexes, en tenant compte des interactions réelles entre leurs composants : partage, dépendances et coordination. Au LMF, Mihaela Sighireanu pilote la contribution du laboratoire, centrée sur des techniques de vérification fondées sur des logiques de séparation étendues. Cette approche vise une analyse à la fois plus expressive et plus automatisable des systèmes en évolution. Pour en savoir plus, consultez la présentation du projet et les sites de ses partenaires : LIG, VERIMAG et LORIA.

Raghda El Shehaby (TU Wien, Institute of Computer Engineering), Matthias Függer (LMF, CNRS, ENS Paris-Saclay), Florian Huemer (TU Wien, Institute of Computer Engineering) and Andreas Steininger (TU Wien, Institute of Computer Engineering) received the Best IEEE ASYNC Paper Award in 2025. Read more...

C'est avec une immense tristesse que nous avons appris le décès de notre collègue Gilles Dowek, survenu le 21 juillet 2025.

Directeur de recherche chez Inria, professeur attaché à l’ENS Paris-Saclay, fondateur de l’équipe Deducteam et membre du Laboratoire Méthodes Formelles, Gilles Dowek a contribué de manière exceptionnelle à l'essor scientifique de la discipline informatique. Read more...

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.

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?

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

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

Synthesis for Games of Imperfect Information under Full-Information Protocols

Jul 7 14:00 ₂₀₂₅

Monday 7 July 2025 at 14h00
ENS Paris-Saclay, Room 1B36 and online

Abstract: Different models can be used to represent programs, to check their correctness, or even better to synthesise them from a specification. Here, we model a program as a player against an environment. Constructing a correct program then boils down to synthesising a winning strategy in the associated game, that is, a behaviour that ensures that the winning condition is satisfied regardless of the behaviour of the environment.

We introduce a new class of games where the player receives imperfect information by communicating with passive observers in a full-information protocol. Unlike the classical model, the player can in one moment obtain an unbounded amount of information.

Read more...

The LMF seminar 2025 takes place on June 2-3, 2025 at Centre Port Royal in Saint-Lambert.

Read more...