Bienvenue L'IRIF est une unité mixte de recherche (UMR 8243) entre le CNRS et l'Université Paris Cité, et héberge une équipe-projet Inria. Les recherches menées à l'IRIF reposent sur l’étude et la compréhension des fondements de toute l’informatique, afin d’apporter des solutions innovantes aux défis actuels et futurs des sciences numériques. L'IRIF regroupe près de deux cents personnes. Sept de ses membres ont été lauréats de l'European Research Council (ERC), trois sont membres de l'Institut Universitaire de France (IUF), deux sont membres de l'Academia Europæa, et un est membre de l'Académie des sciences. Notion du jour Réseaux Sociaux Suivez nous sur LinkedIn, Bluesky et Mastodon : Actualités 14.3.2025 Le troisième épisode du podcast “Qu'est ce que tu cherches ?” du CNRS a invité Geoffroy Couteau pour parler de son sujet de recherche : la protection des données privées, les calculs sécurisés, les protocoles sécurisés. Vous pourrez également découvrir sa journée type, le moment où il fait le plus de sciences (et non, ce n'est pas forcément pendant la journée !), les stéréotypes liés à son domaine. (Ré)Écoutez cet épisode : 10.3.2025 Félicitations à Florian Horn, co-auteur de Revelations: A Decidable Class of POMDPs with Omega-Regular Objectives, papier récompensé par le prix “Outstanding Paper Awards” à AAAI 2025. 18.2.2025 A l'occasion du colloque du CNRS intitulé « L'optimisation, au cœur des défis des sciences informatiques », Simon Apers, chargé de Recherche CNRS à l'IRIF a réalisé une présentation Flash'Opti de trois minutes sur l'apport des algorithmes quantiques à l'optimisation. Les présentations Flash'Opti sont un concept original du CNRS visant à présenter un sujet de recherche en trois minutes, à l'aide d'une seule image. Revisionnez son intervention: 30.1.2025 Félicitations à Esaïe Bauer et Alexis Saurin dont le papier à été accepté pour la conférence FoSSaCS 2025 ! 17.2.2025 La vulgarisation scientifique, pour tous les âges ! Sophie Laplante, professeure à l'IRIF, a contribué au numéro 425 de Science & Vie Junior, qui consacre un article au quantique. Après une BD introductive, place aux explications pour mieux comprendre l’ordinateur quantique et démystifier ses promesses. Chiffrement, clés, données, calculs et bits… Ces concepts sont expliqués de façon accessible, pour permettre à tous, petits et grands, d’explorer les mystères du quantique en toute simplicité ! À découvrir dans Science & Vie : 10.2.2025 Félicitations à Adrian Vladu, membre de l'IRIF, dont l'article a été accepté à STOC 2025, une conférence ACM : 30.1.2025 Trois articles de membres de l'IRIF ont été acceptés à ESOP 2025. Félicitations à Giovanni Bernardi, Thomas Ehrhard, Claudia Faggian et Giulia Manara ! 18.2.2025 A l'occasion du colloque du CNRS intitulé « L'optimisation, au cœur des défis des sciences informatiques », David Saulpic, chargé de recherche CNRS à l'IRIF, a réalisé une présentation Flash'Opti de trois minutes sur le Big Data. Les présentations Flash'Opti sont un concept original du CNRS visant à présenter un sujet de recherche en trois minutes, à l'aide d'une seule image. Revisionnez son intervention: edit toutes les anciennes actualités (Ces actualités sont présentées selon un classement mêlant priorité et aléatoire.) Agenda Preuves, programmes et systèmes Jeudi 27 mars 2025, 10 heures 30, Salle 3052 & online (Zoom link) Andrei Paskevich (LMF, Université Paris-Saclay, Inria Saclay) Coma, an Intermediate Verification Language with Explicit Abstraction Barriers We introduce Coma, a formally defined intermediate verification language. Specification annotations in Coma take the form of assertions mixed with the executable program code. A special programming construct representing the abstraction barrier is used to separate, inside a subroutine, the “interface” part of the code, which is verified at every call site, from the “implementation” part, which is verified only once, at the definition site. In comparison with traditional contract-based specification, this offers us an additional degree of freedom, as we can provide separate specification (or none at all) for different execution paths. For programs where specification is given in a traditional way, with abstraction barriers at the function entries and exits, our verification conditions are similar to the ones produced by a classical weakest-precondition calculus. For programs where abstraction barriers are placed in the middle of a function definition, the user-written specification is seamlessly completed with the verification conditions generated for the exposed part of the code. In the talk, we present the language, the rules of verification condition generation, and the current implementation of Coma. Séminaire des membres non-permanents Jeudi 27 mars 2025, 16 heures, Salle 3052 Maria Clara Werneck From political representation fairness to symbolic dynamical systems In many countries, the union is divided into states, and the number of deputies in the federal congress depends on the state. Imagine that each year, a congressperson is elected to be the chair of the congress. The challenge is to assign this role in such a way that, at any given time, the accumulated number of chairpersons from each state remains proportional to its assigned weight. This is known as the chairperson assignment problem. In this talk, we will introduce a metric for quantifying fairness in this context and explain its connection to symbolic dynamics. This presentation will also be an introduction to symbolic dynamical systems. Catégories supérieures, polygraphes et homotopie Vendredi 28 mars 2025, 14 heures, Salle 1013 Yann Palu (Université d'Amiens (LAMFA)) Catégories extriangulées 0-Auslander Cet exposé est une introduction au catégories extriangulées. La notion de catégorie exacte (au sens de Quillen) est une axiomatisation des sous-catégories de catégories abéliennes, stables par extensions. Le catégories extriangulées sont une tentative d'axiomatisation analogue adaptée au cas des sous-catégories de catégories triangulées, stables par extensions. Après avoir donné des exemples provenant de la combinatoire et de la théorie des représentations, j'expliquerai cette axiomatisation et montrerai comment elle peut être utilisée dans des situations variées. Il s'agit de plusieurs travaux en commun avec Hiroyuki Nakaoka et avec Xin Fang, Misha Gorsky, Osamu Iyama, Arnau Padrol, Vincent Pilaud, Pierre-Guy Plamondon, Matt Pressland. Automates Vendredi 28 mars 2025, 14 heures, Salle 3052 Mahsa Shirmohammadi The Complexity of Orbit-Closure Problems Computational problems concerning the orbit of a point under the action of a matrix group occur in numerous subfields of computer science, including complexity theory, program analysis, quantum computation, and automata theory. In many cases the focus extends beyond orbits proper to orbit closures under a suitable topology. Typically one starts from a group and several points and asks questions about the orbit closure of the points under the action of the group, e.g., whether two given orbit closures intersect. In this talk, I will introduce and motivate several problems involving groups and orbit closures, focusing on computation and determination tasks. In regards to computation, we are given a set of matrices and tasked with computing the defining ideal of the algebraic group generated by those matrices. The determination task, on the other hand, involves starting with a given variety and determining whether and how it can be represented as an algebraic group or an orbit closure. The “how” question often asks whether the underlying group can be topologically generated by s matrices for a given s. The talk is based on several joint works: (ISSAC 22) https://dl.acm.org/doi/10.1145/3476446.3536172 (Submitted) https://arxiv.org/abs/2407.04626 (POPL25) https://arxiv.org/abs/2407.09154 Combinatoire énumérative et analytique Mardi 1 avril 2025, 14 heures, Salle 3071 Fufa Beyene (Université D'Addis Ababa) Familles de partitions d’ensembles de type B comptées par les nombres de Dowling (shiftés) Algorithmes et complexité Mardi 1 avril 2025, 11 heures, Salle 3052 Mohammad Reza Mousavi (King's College London) Taming Spooky Actions at a Distance: A Discipline of Quantum Software Testing We are witnessing the increased availability of powerful quantum computing facilities as a service; also, there are promising prospects of applying quantum computing in fields such as material- and drug discovery, as well as scheduling, and optimisation. With these prospects comes an inherent challenge of quality assurance of complex quantum programs. Quantum programs and programming frameworks are becoming more complex, and this complexity creates a gap, calling for novel and rigorous testing and debugging frameworks. In this talk, we present an overview of the fascinating emerging field of software engineering and its numerous challenges and opportunities. In particular, we review our recent research on characterising faults in hybrid quantum-classical architectures. This has led to a taxonomy of real faults in hybrid quantum-classical architectures. We also present our long-standing effort to establish a mature property-based testing framework for quantum programs both for fault-tolerant and for noisy architecture. We also present an automated debugging framework based on property-based testing. Algorithmique distribuée et graphes Mardi 1 avril 2025, 15 heures, 3052 Clara Marcille (Bordeaux) Graph Irregularity via Edge Deletions In graph modification problems, we want to modify a graph through some operation (e.g. vertex/edge deletion/addition/contraction) to obtain a graph belonging to some specific class of graphs. Here, we pursue the study of edge-irregulators of graphs, which were recently introduced in [Fioravantes et al. Parametrised Distance to Local Irregularity. {\it IPEC}, 2024]. That is, we are interested in the parameter ${\rm I}_e(G)$, which, for a given graph $G$, denotes the smallest $k \geq 0$ such that $G$ can be made locally irregular (\textit{i.e.}, with no two adjacent vertices having the same degree) by deleting $k$ edges. We exhibit notable properties of interest of the parameter ${\rm I}_e$, in general and for particular classes of graphs. Our investigation leads us to propose a conjecture that $\ie(G)$ should always be at most $\frac{1}{3}m+c$, where $m$ is the size of the graph $G$ and $c$ is some constant. We verify this conjecture in the case of paths, cycles, trees and complete graphs, and we provide the first step towards proving the conjecture for cubic graphs. Finally, we present a linear-time algorithm that computes $\ie(G)$ when $G$ is a tree of bounded maximum degree. One world numeration seminar Mardi 1 avril 2025, 14 heures, Online Meng Wu (Oulun yliopisto) On normal numbers in fractals Let $K$ be the ternary Cantor set, and let $\mu$ be the Cantor–Lebesgue measure on $K$. It is well known that every point in $K$ is not 3-normal. However, if we take any natural number $p \ge 2$ that is not a power of 3, then $\mu$-almost every point in $K$ is $p$-normal. This classical result is due to Cassels and W. Schmidt. Another way to obtain normal numbers from K is by rescaling and translating $K$, then examining the transformed set. A recent nice result by Dayan, Ganguly, and Barak Weiss shows that for any irrational number $t$, for $\mu$-almost all $x \in K$, the product $tx$ is 3-normal. In this talk, we will discuss these results and their generalizations, including replacing $p$ with an arbitrary beta number and considering more general times-3 invariant measures instead of the Cantor–Lebesgue measure. Soutenances de thèses Vendredi 4 avril 2025, 14 heures, Amphithéâtre Gouges 1, Bâtiment Olympe de Gouges Corentin Henriet (IRIF) Planar maps, Tamari intervals and parking trees: a bijective journey As the title suggests, this thesis is an exploration of the bijective links between three families of combinatorial objects: planar maps, Tamari intervals and parking trees. Along the way, we will encounter many other kinds of combinatorial animals with exotic names, such as fighting fish, quadrant excursions, embedded mobiles, closed flows and blossoming trees… Planar maps have been well known to combinatorialists since they were intro- duced about sixty years ago. Their rich underlying combinatorial structure has contributed to the development of a strong bijective framework surrounding them. We can cite the examples of bijections with blossoming trees, which allow elegant proofs of beautiful formulas counting families of planar maps. More recently, the discovery of similar formulas for Tamari intervals has led to the exploration of the bijective connection with planar maps. In this manuscript, we revisit some of these bijections and create new ones, shedding new light by integrating numerous combi- natorial families. At the crossroads of the correspondences developed in our work, we will en- counter several models of parking trees. Not only do these trees appear naturally to encode families of planar maps and Tamari intervals, but they are also proto- types of objects governed by catalytic equations. In this sense, the general study of parking trees, initiated by Duchi and Schaeffer in 2023, and continued here, seems very promising for a further refined understanding of the bijective and enumerative schemes surrounding this manuscript. Algorithmique distribuée et graphes Mardi 8 avril 2025, 15 heures 30, 3052 Laurent Viennot (IRIA et IRIF) Certificates in P and Subquadratic-Time Computation of Radius, Diameter, and all Eccentricities in Graphs In the context of fine-grained complexity, we investigate the notion of certificate enabling faster polynomial-time algorithms. We specifically target radius (minimum eccentricity), diameter (maximum eccentricity), and all-eccentricity computations for which quadratic-time lower bounds are known under plausible conjectures. In each case, we introduce a notion of certificate as a specific set of nodes from which appropriate bounds on all eccentricities can be derived in subquadratic time when this set has sublinear size. The existence of small certificates for radius, diameter and all eccentricities is a barrier against SETH-based lower bounds for these problems. We indeed prove that for graph classes with certificates of bounded size, there exist randomized subquadratic-time algorithms for computing the radius, the diameter, and all eccentricities respectively. Moreover, these notions of certificates are tightly related to algorithms probing the graph through one-to-all distance queries and allow to explain the efficiency of practical radius and diameter algorithms from the literature.