News

Mathematical modeling of microalgal growth – hybrid and data-driven approaches for multi-scale prediction

Nov 23 14:00 ₂₀₂₆

Monday, 23 November, 2pm
Amphi Dorothy Hodgkin, ENS Paris-Saclay, Gif-sur-Yvette and online

Abstract: Microalgae have numerous applications, ranging from wastewater treatment to the production of proteins and biofuels. Developing these applications requires a better understanding and prediction of microalgal growth, particularly when moving from laboratory cultures to larger-scale systems. Read more...

Formal methods for psychology and consciousness science

Nov 30 9:00 ₂₀₂₆

Monday, November 30st, 9am
Room 1B26, ENS Paris-Saclay, Gif-sur-Yvette

Abstract: Psychological and neurocognitive theories are frequently stated in natural language. Such verbal theories often contain ambiguities and leave key components underspecified, which makes them difficult to validate or falsify. This thesis introduces a framework to formally build and analyze some parts of psychological and neurocognitive theories, drawing on formal methods from theoretical computer science: communicating, timed, and probabilistic automata, refinement, and model checking. Read more...

Théo Winterhalter, chercheur au LMF, reçoit un Distinguished-Paper Award à la conférence POPL 2026 (Symposium on Principles of Programming Languages) pour l'article :

"Encode the Cake and Eat It Too: Controlling Computation in Type Theory, Locally" Yann Leray, Théo Winterhalter dl.acm.org/doi/10.1145/3776704

À propos du prix

At most 10% of the accepted papers of POPL 2026 will be designated as Distinguished Papers. This award highlights papers that the Review Committee thinks should be read by a broad audience due to their relevance, originality, significance, and clarity. The selection of the distinguished papers will be made based on the final version of the paper and through an additional review process.

Toutes nos félicitations à Théo Winterhalter et Yann Leray pour cette reconnaissance !

Dans le numéro de juin 2026 de Communications of the ACM, Christine Paulin-Mohring revient sur quarante ans de développement de Rocq (anciennement Coq), l'un des assistants de preuve les plus utilisés pour vérifier formellement la correction de programmes et de démonstrations mathématiques. Elle y évoque ses contributions fondatrices, son travail sur la bibliothèque ALEA pour les programmes probabilistes, et l'évolution des usages de Rocq, aujourd'hui mobilisé aussi bien pour la vérification de compilateurs que pour l'enseignement des mathématiques.

Lire l'entretien complet sur Communications of the ACM.

Stéphane Demri, CNRS researcher at LMF, has published Concise Introduction to Alternating-Time Temporal Logics: A Guide for Understanding the Model-Checking Problem.

From the publisher’s description: ''This textbook provides a concise presentation of alternating-time temporal logics dedicated to strategic reasoning in multi-agent systems. Read more...

The annual program verification competition VerifyThis took place in Turin, as part of ETAPS 2026. Among 24 participating teams, two teams from LMF received prizes, including the main award:

• Best Overall Team: Li-yao Xia and Jacques-Henri Jourdan
• Best One-Person Team: Jean-Christophe Filliâtre

Read more...

© Laurent Ardhuin pour le CNRS

Patricia Bouyer-Decitre (LMF, CNRS, ENS Paris-Saclay) has been awarded the CNRS Silver Medal 2026 in recognition of her contributions to formal methods, automata theory, logic, and game theory. Read more...

Translations of Proofs between Higher-Order Logics and between Theories with Rewriting

Sep 24 14:00 ₂₀₂₆

Thursday, 24 September 2026 at 2pm
Amphi 1, Eiffel building, CentraleSupélec, Gif-sur-Yvette

Abstract: Formal proofs and proof assistants are rigorous tools for expressing theorems and verifying their validity. Formal proofs can be based on a wide variety of logics, implemented in various proof assistants, and use numerous data structures or representations. Read more...

Quantum Cellular Automata and Quantum Field Theories

Sep 24 14:00 ₂₀₂₆

Thursday, 24 September 2026 at 2pm
Room 1B26, ENS Paris-Saclay, 4 Av. des Sciences, 91190 Gif-sur-Yvette

Abstract: This thesis studies Quantum Cellular Automata (QCAs) as discrete-spacetime, strictly local, and unitary models of quantum field theories, with a focus on lattice artifacts, their resolution, and the digital quantum simulation of gauge theories.

Read more...

James Hefford et Matt Wilson, chercheurs au LMF, ont été interviewés par New Scientist suite à la publication de leur article :

Decoherence to quantum theory from a causally indefinite post-quantum theory James Hefford, Matt Wilson, Physical Review A, 2026, 113 (4), pp.042433 10.1103/kmmy-3dy3

À lire sur New Scientist : archive.ph/UwVm6

LMF Seminar 2026

Read more...

Vérification pratique de transformations de circuits quantiques

Jun 4 14:00 ₂₀₂₆

Jeudi 4 juin 2026 à 14h00, heure de Paris
Salle 1Z61, École normale supérieure Paris-Saclay, 4 Av. des Sciences, 91190 Gif-sur-Yvette

Le lien de visioconférence et les informations pratiques seront disponibles sur la page de la soutenance : https://jricc.github.io/github.io

Résumé : Ma thèse porte sur la vérification formelle des transformations de circuits quantiques. Ces transformations sont essentielles en compilation, optimisation ou adaptation au matériel, mais elles peuvent modifier le comportement du circuit. Read more...

Jun 19 9:00 ₂₀₂₆

A colloquium in memory of Gilles Dowek (1966–2025) will be held on 19 June 2026 at ENS Paris-Saclay.

The event will bring together colleagues, collaborators, and former students to reflect on his influential contributions to computer science, logic, and philosophy. Gilles Dowek made important advances in type theory and automated reasoning, and was also deeply involved in education. The colloquium will highlight the breadth of his work and its lasting impact. Further information is available on the event webpage: https://deducteam.gitlabpages.inria.fr/colloque-gilles/

Jun 10 9:00 ₂₀₂₆

The 1st Workshop on Computational Psychology will take place on June 10th 2026 at ENS Paris-Saclay. Computational Psychology is an interdisciplinary framework that formalizes psychological processes through explicit computational structures.

Situated at the intersection of theoretical psychology, computer science, and data science, it seeks to transform psychological theories into well-defined systems capable of simulation and empirical testing. For information on the programme and registration, visit https://compsych.sciencesconf.org.

Jun 17 9:00 ₂₀₂₆ Jun 18 18:00 ₂₀₂₆

LHC is a French workgroup about logic, homotopy and categories. It brings together researchers in France who work on connecting theoretical computer science, topology, and

category theory to study the theoretical foundations of programming languages, logic, and their semantics. The seventh edition of the LHC days will take place on Wednesday 17 and Thursday 18 June 2026. For information on the programme and registration, visit https://smimram.gitlabpages.inria.fr/lhc/journees.html.

Jun 2 13:00 ₂₀₂₆ Jun 3 9:00 ₂₀₂₆

GT DAAL, the Working Group on Data, Automata, Algebra, and Logic, gathers the French community working on mathematical foundations for the verification of programs and databases.

Topics include database theory, automata theory (words, trees, orders, quantitative and probabilistic models), logic (specification and query formalisms, model theory, model checking, satisfiability, containment, synthesis), games (in logic, verification, model theory, set theory), and algebra and topology. The annual meeting of GT DAAL will be held at ENS Paris-Saclay, in auditorium 1B26, on 2–3 June 2026. For information on the programme, visit https://lmf.cnrs.fr/DAAL2026/.

Vérification formelle des systèmes complexes

Feb 10 10:30 ₂₀₂₆

Mardi 10 février 2026 à 10h30
ENS Paris-Saclay, Salle 1B26, and online

Résumé : La vérification des systèmes complexes est devenue un enjeu majeur en informatique, car les applications modernes intègrent de plus en plus d'hétérogénéité, d'incertitude et de composants d'apprentissage. Mes recherches abordent ce défi selon trois axes complémentaires : les systèmes partiellement observés, la vérification probabiliste et l'analyse formelle des systèmes d'apprentissage.

Dans un premier temps, j'ai étudié la diagnosticabilité et la prédictibilité en étendant les cadres classiques à des contextes actifs et quantitatifs. J'ai proposé et développé un nouveau cadre d'abstraction-raffinement évolutif (basé sur CEGAR) pour la vérification de la diagnosticabilité des automates temporisés. Son efficacité a été démontrée par des expérimentations sur des jeux de données de référence construits, comblant ainsi le fossé entre complexité théorique et applicabilité pratique. La seconde orientation porte sur les modèles probabilistes, notamment les chaînes de Markov à états infinis, où j'ai étudié le calcul des probabilités d'accessibilité à travers deux propriétés sémantiques: la decisiveness et la divergence. Il convient de noter que la decisiveness a fait l'objet d'une analyse approfondie permettant d'obtenir de nouveaux résultats significatifs, et que la divergence a été introduite et examinée, ces deux éléments ouvrant la voie à des algorithmes génériques pour calculer l’approximation de l'accessibilité. Enfin, je me suis également intéressé à l'exploration de la vérification formelle des systèmes d'apprentissage, en abordant à la fois l'amélioration des performances de la vérification des réseaux de neurones et l'analyse de la robustesse des algorithmes d'apprentissage.

Ensemble, ces contributions visent à établir un cadre unifié pour la vérification formelle et fiable des systèmes dynamiques, stochastiques et d'apprentissage.

Jury :

• Benoît Delahaye, Professeur des Universités, Nantes Université - LS2N (Rapporteur)
• Eric Fabre, Directeur de recherche, Centre Inria de l'Université de Rennes (Rapporteur)
• Louise Travé-Massuyès, Directrice de recherche, LAAS-CNRS (Rapporteuse)
• Béatrice Bérard, Professeur émérite, Sorbonne Université., LIP6 - CNRS (Examinatrice)
• Nathalie Bertrand, Directrice de recherche, Centre Inria de l'Université de Rennes et IRISA (Examinatrice)
• Julien Signoles, Directeur de recherche, Université Paris-Saclay, CEA, List (Examinateur)