Institut de Recherche en Informatique Fondamentale (IRIF)

CNRS

Université Paris Cité

IRIF is a research laboratory of CNRS and Université Paris Cité, also hosting one Inria project-team.

The research conducted at IRIF is based on the study and understanding of the foundations of all computer science, in order to provide innovative solutions to the current and future challenges of digital sciences.

IRIF hosts about 200 people. Seven of its members have been distinguished by the European Research Council (ERC), six are members of the Institut Universitaire de France IUF), two are members of the Academia Europæa, and one is member of Académie des sciences.

Follow us on Twitter/X, LinkedIn and Mastodon for our latest news:

LinkedIn Twitter/X Mastodon

podcast_geoffroycouteau.jpg

14.3.2025
The third episode of the CNRS podcast “Qu'est-ce que tu cherches ?” features Geoffroy Couteau, who talks about his research on data privacy protection, secure computations, and secure protocols. You will also get a glimpse into his typical day, the time when he is most productive in science (and no, it's not necessarily during the day!), and the stereotypes associated with his field. (Re)listen to this episode:

aaai_2025.jpg

10.3.2025
Congratulations to Florian Horn, co-author of Revelations: A Decidable Class of POMDPs with Omega-Regular Objectives, a paper awarded the “Outstanding Paper Awards” at AAAI 2025.

30.1.2025
Congratulations to Esaïe Bauer and Alexis Saurin, whose paper has been accepted for the FoSSaCS 2025 conference!

18.2.2025
For the CNRS conference titled « L’optimisation, au cœur des défis des sciences informatiques » (Optimization, at the core of the challenges of computer science), David Saulpic, a CNRS Research Scientist at IRIF delivered a three-minute Flash'Opti presentation about Big Data. The Flash'Opti presentations are a CNRS original concept designed to showcase a research topic in just three minutes, using the support of a single image. Take another look at his intervention:

stoc_2025.jpg

10.2.2025
Congratulations to the Adrian Vladu, IRIF member, whose paper have been accepted to STOC 2025, an ACM conference:

17.2.2025
Science popularization for all ages! Sophie Laplante, professor at IRIF, contributed to issue 425 of Science & Vie Junior, which features an article on quantum science. After an introductory comic, it's time for clear explanations to better understand the quantum computer and demystify its promises. Encryption, keys, data, computations, and bits… These concepts are presented in an accessible way, allowing everyone, young and old, to explore the mysteries of quantum science with ease! Discover it in Science & Vie!

30.1.2025
Three papers of IRIF Members have been accepted to ESOP 2025. Congratulations to Giovanni Bernardi, Thomas Ehrhard, Claudia Faggian and Giulia Manara!

cnrs_editions_lecalculadecouvert.jpg

10.2.2025
CNRS EDITIONS has published a new book on the history of calculation, titled 𝐿𝑒 𝑐𝑎𝑙𝑐𝑢𝑙 𝑎̀ 𝑑𝑒́𝑐𝑜𝑢𝑣𝑒𝑟𝑡. Several current and former IRIF researchers contributed to the writing of this book by authoring chapters:
◻️ Part 4: ▪️ Chapter 1 - 𝑳'𝒂𝒍𝒈𝒐𝒓𝒊𝒕𝒉𝒎𝒆 : 𝒗𝒆𝒓𝒔 𝒍𝒂 𝒓𝒆́𝒔𝒐𝒍𝒖𝒕𝒊𝒐𝒏 𝒄𝒐𝒏𝒄𝒓𝒆̀𝒕𝒆 𝒅𝒆 𝒑𝒓𝒐𝒃𝒍𝒆̀𝒎𝒆𝒔 – Claire Mathieu
▪️ Chapter 2 - 𝑳𝒂 𝒄𝒐𝒎𝒑𝒍𝒆𝒙𝒊𝒕𝒆́ 𝒂𝒍𝒈𝒐𝒓𝒊𝒕𝒉𝒎𝒊𝒒𝒖𝒆 – Sylvain Perifel
◻️ Part 9: ▪️ Chapter 1 - 𝑳𝒆𝒔 𝒇𝒐𝒏𝒅𝒆𝒎𝒆𝒏𝒕𝒔 𝒅𝒖 𝒄𝒂𝒍𝒄𝒖𝒍 𝒒𝒖𝒂𝒏𝒕𝒊𝒒𝒖𝒆 – Frédéric Magniez

(These news are displayed using a randomized-priority ranking.)

Algorithms and complexity
Wednesday March 26, 2025, 11AM, 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.

Algorithms and complexity
Wednesday March 26, 2025, 10AM, 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.

Graphs and Logic
Wednesday March 26, 2025, 1:30PM, 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.

Proofs, programs and systems
Thursday March 27, 2025, 10:30AM, 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.

Non-permanent members' seminar
Thursday March 27, 2025, 4PM, 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.

Higher categories, polygraphs and homotopy
Friday March 28, 2025, 2PM, 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.

Automata
Friday March 28, 2025, 2PM, 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

Algorithms and complexity
Tuesday April 1, 2025, 11AM, 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.

Distributed algorithms and graphs
Tuesday April 1, 2025, 3PM, 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
Tuesday April 1, 2025, 2PM, 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.