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. 30.1.2025 Félicitations à Esaïe Bauer et Alexis Saurin dont le papier à été accepté pour la conférence FoSSaCS 2025 ! 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: 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: 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 : 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 ! 10.2.2025 CNRS EDITIONS a publié un nouvel ouvrage sur l'histoire du calcul, intitulé 𝐿𝑒 𝑐𝑎𝑙𝑐𝑢𝑙 𝑎̀ 𝑑𝑒́𝑐𝑜𝑢𝑣𝑒𝑟𝑡. Plusieurs chercheurs actuels et anciens de l'IRIF ont contribué à la rédaction de ce livre en rédigeant des chapitres : ◻️ Partie 4 : ▪️ Chapitre 1 - 𝑳'𝒂𝒍𝒈𝒐𝒓𝒊𝒕𝒉𝒎𝒆 : 𝒗𝒆𝒓𝒔 𝒍𝒂 𝒓𝒆́𝒔𝒐𝒍𝒖𝒕𝒊𝒐𝒏 𝒄𝒐𝒏𝒄𝒓𝒆̀𝒕𝒆 𝒅𝒆 𝒑𝒓𝒐𝒃𝒍𝒆̀𝒎𝒆𝒔 - Claire Mathieu ▪️ Chapitre 2 - 𝑳𝒂 𝒄𝒐𝒎𝒑𝒍𝒆𝒙𝒊𝒕𝒆́ 𝒂𝒍𝒈𝒐𝒓𝒊𝒕𝒉𝒎𝒊𝒒𝒖𝒆 - Sylvain Perifel ◻️ Partie 9 : ▪️ Chapitre 1 - 𝑳𝒆𝒔 𝒇𝒐𝒏𝒅𝒆𝒎𝒆𝒏𝒕𝒔 𝒅𝒖 𝒄𝒂𝒍𝒄𝒖𝒍 𝒒𝒖𝒂𝒏𝒕𝒊𝒒𝒖𝒆 - Frédéric Magniez edit toutes les anciennes actualités (Ces actualités sont présentées selon un classement mêlant priorité et aléatoire.) Agenda Algorithmes et complexité Mercredi 26 mars 2025, 11 heures, Salle 3052 Arjan Cornelissen (Simons Institute, UC Berkeley) Quantum algorithms through graph composition In this talk, I will give a glimpse of an ongoing project on the development of quantum algorithms through the composition of graphs. At a high level, the idea is to represent a quantum query algorithm as a graph. The graph composition framework, that this work introduces, then provides a black-box way to turn such graphs into quantum algorithms. It turns out that this framework is able to unify many existing frameworks that generate quantum query algorithms, and it provides tangible ways to make these implementations time-efficient too. If time permits, we will also take a look at several examples for which this framework can be used. Algorithmes et complexité Mercredi 26 mars 2025, 10 heures, Salle 3052 Joseph Cunningham (ULB, Brussels) Unstructured Adiabatic Quantum Optimization: Optimality with Limitations In the circuit model of quantum computing, amplitude amplification techniques can be used to find solutions to NP-hard problems defined on $n$-bits in time $\mathrm{poly}(n)2^{n/2}$. In this work, we investigate whether such general statements can be made for adiabatic quantum optimization, as provable results regarding its performance are mostly unknown. Although a lower bound of $\Omega(2^{n/2})$ has existed in such a setting for over a decade, a purely adiabatic algorithm with this running time has been absent. We show that adiabatic quantum optimization using an unstructured search approach results in a running time that matches this lower bound (up to a polylogarithmic factor) for a broad class of classical local spin Hamiltonians. For this, it is necessary to bound the spectral gap throughout the adiabatic evolution and compute beforehand the position of the avoided crossing with sufficient precision so as to adapt the adiabatic schedule accordingly. However, we show that the position of the avoided crossing is approximately given by a quantity that depends on the degeneracies and inverse gaps of the problem Hamiltonian and is NP-hard to compute even within a low additive precision. Furthermore, computing it exactly (or nearly exactly) is #P-hard. Our work indicates a possible limitation of adiabatic quantum optimization algorithms, leaving open the question of whether provable Grover-like speed-ups can be obtained for any optimization problem using this approach. Graphes et Logique Mercredi 26 mars 2025, 13 heures 30, salle 3052 Sylvain Schmitz; Giannos Stamoulis Well quasi-orders and preservation theorems for First-Order Logic; Some extensions of First-Order logic on graphs This will be a gentle tutorial on mostly standard results about well-quasi-orders (wqo) in a context of graph theory and algorithmic meta-theorems. I intend to cover a few basics of wqo theory, their applications in algorithmic graph theory, a focus on classes of graphs that are well-quasi-ordered by the induced subgraph ordering, along with Pouzet's Conjecture, and finally the generalisation to preservation properties in first-order logic. . In this tutorial we present a landscape of extensions of first-order logic (on graphs) and we discuss their expressive power and algorithmic results related to them. These extensions involve either additional predicates expressing different types of connectivity or the quantification over vertex sets that are (in a sense) of simple structure. 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 Non encore annoncé. 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 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.