News
PhD Defense: Josué Moreau
Programming language and formally verified compiler for low-level numerical libraries
Tuesday 25 November 2025 at 14h00
ENS Paris-Saclay, Room 1Z76 and online
Abstract: Low-level numerical libraries like GMP and BLAS are widely used. They are mostly written in C, Fortran, and Assembly, and make a heavy use of arrays and pointers. These languages are well-suited for writing efficient code but they are not safe, that is, they have many undefined behaviors, which increase the chance for bugs. Read more...
PhD Defence: Marin Costes
Causal graph rewriting: Space-time determinism and reversibility
Tuesday 2 December 2025 at 10h30
Amphi building 660 and online
Abstract: We study non-terminating graph rewriting models, whose local rules are applied non-deterministically---and yet enjoy a strong form of determinism, namely space-time determinism. For terminating computation, it is well-known that the property of confluence may ensure a deterministic end result. In the context of distributed, non-terminating computation however, confluence alone is too weak a property. In this thesis we provide sufficient conditions so that asynchronous local rule applications produce well-determined events in the space-time unfolding of the graph, regardless of their application orders.
PhD Defense: Zhuofan Xu
Permutation equivariant and permutation invariant reinforcement learning for multi-agent systems
Thursday 11 December 2025 at 9h00
ENS Paris-Saclay, Room 1Z25 and online
Abstract: Deep Reinforcement Learning (DRL) has achieved remarkable success in sequential decision-making tasks, from games to robotics. Extending DRL to Multi-Agent Reinforcement Learning (MARL) introduces additional challenges: agents must coordinate in high-dimensional environments, training becomes unstable due to non-stationarity, and learned strategies often fail to generalize across team sizes or tasks.
CNRS Focus on the ANR-NARCO project
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.
Focus Sciences sur le projet ANR-NARCO
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.
Best-Paper Award at ASYNC 2025
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...
Décès de Gilles Dowek
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...
Prix de thèse du GDR GPL pour Mickaël Laurent
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.
Science flash: Where does time actually come from?
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.
PhD Defense: Luc Chabassier
Aspects of Category Theory in Proof Assistants
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.
Best-Paper Award at ETAPS 2025
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...
PhD Defense: Thomas Soullard
Synthesis for Games of Imperfect Information under Full-Information Protocols
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.
Séminaire au vert, Port Royal à Saint-Lambert, 2 – 3 juin 2025
The LMF seminar 2025 takes place on June 2-3, 2025 at Centre Port Royal in Saint-Lambert.
