News
PhD Defense Thomas Traversié
Translations of Proofs between Higher-Order Logics and between Theories with Rewriting
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. The goal of this thesis is to design translations of formal proofs between such formalisms.
PhD Defense Dogukan Bakircioglu
Quantum Cellular Automata and Quantum Field Theories
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.
We extend the gauged-QCA framework to non-Abelian symmetries, building the first QCA model coupling (1+1)D Dirac fermions to an SU(2) Yang–Mills gauge field.
Distinguished-Paper Award à POPL 2026 pour Théo Winterhalter
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 !
Entretien avec Christine Paulin-Mohring dans Communications of the ACM
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.
New book by Stéphane Demri on alternating-time temporal logics
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...LMF members win at VerifyThis 2026
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
Patricia Bouyer-Decitre receives CNRS Silver Medal 2026
© 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. This prestigious distinction honors researchers for the originality, quality, and impact of a body of work that significantly advances research at the national and international levels.
Événements passés
Un article du LMF dans New Scientist
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
PhD Defense Jérome Ricciardi
Vérification pratique de transformations de circuits quantiques
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...
Colloquium in memory of Gilles Dowek
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/
1st Workshop on Computational Psychology
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.
Annual meeting of GT LHC
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.
Annual meeting of GT DAAL
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/.
Soutenance HDR Lina Ye
Vérification formelle des systèmes complexes
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)
PhD Defense: Quentin Petitjean
Automated Tools for Inductive Reasoning in Separation Logic
Friday 30 January 2026 at 14h00
ENS Paris-Saclay, Amphi 1B26 and online
Abstract: The automated program verification aims to produce formal proofs of correctness for programs with respect to their specifications, requiring minimal user interaction. This technique is based on expressive program logics to capture the properties of programs, and algorithms or heuristics to decide satisfiablity and entailment problem for these logics. Separation logic is one of such logics, specifically designed for reasoning about programs that dynamically allocate memory and mutate this memory through pointers. To specify unbounded memory regions, separation logic includes user-defined predicates, usually expressed through inductive rules. The satisfiability and entailment problems are undecidable in general, but they are decidable for specific fragments. For instance, the PCE fragment is a restriction of the symbolic heap fragment, for which the satisfiability is decidable, where the inductively defined predicates satisfy some syntactic and semantic constraints.
This thesis proposes two extensions of the PCE fragment. The first extension defines a fragment, including the PCE one and formulæ that, although non-PCE, specify data structures that could be represented by PCE formulæ. We propose a procedure attempting to compute an equivalent PCE representation of non-PCE formulæ. We implemented this procedure and tested it on a benchmark of SL formulæ. The second extension supports the specification of overlaid data structures, i.e., data structures that share an unbounded set of locations and are therefore difficult to capture using separating conjunction. The extension, called OSL, introduces an additional operator, the overlaid separating conjunction ✪, which allows for composing heaps that share locations as long as they allocate them with distinct fields. We demonstrate that the OSL fragment has a decidable satisfiability problem.
PhD Defense Gustave Cortal
Traitement automatique des langues pour l'analyse de la subjectivité dans les récits personnels
Mardi 27 janvier 2026 à 14h00
Salle 1B36 - Amphithéâtre Simondon, 4 Av. des Sciences, 91190 Gif-sur-Yvette and online
Résumé : Les récits personnels sont des histoires que les individus racontent sur leurs propres vécus, et qui donnent à voir leurs pensées, sentiments et perceptions. Cette thèse explore des manières de modéliser l'expérience subjective dans les récits personnels à travers le traitement automatique des langues. Nous ancrons d'abord l'analyse des émotions dans les sciences cognitives : nous passons en revue les principales théories des émotions et les relions aux pratiques d'annotation dominantes. De cette synthèse émergent des pistes concrètes pour améliorer les modèles de langue, qu'il s'agisse de nouveaux schémas d'annotation, de méthodologies ou de jeux d'évaluation.