Institut de Recherche en Informatique Fondamentale (IRIF)

CNRS

Université Paris Cité

Welcome

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.

Notion of the day

Social Networks

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

LinkedIn Twitter/X Mastodon

News

dts_omer_reingold.jpg

10.4.2024
IRIF is pleased to announce its second Distinguished Lecture of the year! Our invited speaker is Omer Reingold, professor of computer science at Stanford University and the director of the Simons Collaboration on the Theory of Algorithmic Fairness (Simons Foundation). He will talk about Algorithmic Fairness. Anyone interested is welcome to join us for this talk!

12.4.2024
The rerun of Véronique Cortier Distinguished Talk that was held on February is now available on the IRIF YouTube channel. Her subject was: “Electronic voting: design and formal verification”.

logopintofscience2024.jpg

10.4.2024
Three scientific outreach projects by IRIF researchers have been selected for the 2024 edition of France-Paris Pint of Science. The idea is to discover a scientific theme or subject in a bar. Our researchers will be talking about data protection, graphs and quantum computing.

mirna-dzamonja.jpeg

28.3.2024
The Belgian Mathematical Society (BMS) has awarded Mirna Džamonja (CNRS, IRIF, Université de Paris) with the BMS “Godeaux lecture prize”. “The prize is awarded every year, upon proposal from a BMS board member, to a prominent belgian or international mathematician who is invited to give a talk at a conference in Belgium.” Congratulations!

12.3.2024
Hugo Herbelin, research director at Inria in IRIF, is organizing the next french speaking Horizon Maths day on the topic: Mathematical Proof and Software Safety. It will take place on Wednesday, March 27, 2024, from 9 a.m. to 6 p.m. at the Henri Poincaré Institute (5 rue Pierre et Marie Curie, Paris 5th), Hermite amphitheater. Free but mandatory registration:

podcast_recherche_cm.jpg

19.3.2024
After being increased in September 2023, the budget allocated to the french Higher Education and Research is finally reduced by 904 million euros. The podcast “La Science, CQFD” by France Culture wondered how French research is faring and what direction it is taking. Claire Mathieu, research director at CNRS at IRIF, intervenes.

tayssir_touili.jpg

27.3.2024
We welcome a new research director at IRIF, Tayssir Touili. Her areas of interest are Malware Detection, Software Verification and Formal Methods. You can meet her in room 4028A.

15.3.2024
The 2nd french speaking conference «On éteint, on réfléchit, on discute» organized at Université Paris Cité by François Laroussinie focuses on «Les communs numériques» (“Digital Commons”). Serge Abiteboul and Valerie Peugeot are the invited speakers. It will be held on March 19, 2024, from 4pm to 6pm. This is a free of charge event.

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

Agenda

Verification
Monday April 29, 2024, 11AM, 3052 and Zoom link
Niklas Kochdumper (IRIF) Neural Network Verification using Polynomial Zonotopes

Since artificial intelligence is nowadays also increasingly applied in safety-critical applications such as autonomous driving and human robot collaboration, there is an urgent need for approaches that can efficiently verify that the corresponding neural networks are safe. In general, verification tasks involving neural networks can be classified into the two groups open-loop verification and closed-loop verification. For open-loop verification one aims to prove certain properties of a standalone neural network, while for closed-loop verification the neural network acts as a controller for a dynamic system. This presentation demonstrates a novel verification technique that is based on a polynomial abstraction of the input-output-relation of the single neurons, which proves to be beneficial for both open- as well as closed-loop neural network verification.

Enumerative and analytic combinatorics
Tuesday April 30, 2024, 11AM, Salle 3058
Séminaire Reporté Pas de séance

Algorithms and complexity
Tuesday April 30, 2024, 11AM, Salle 3052
André Chailloux (INRIA Paris) The Quantum Decoding Problem

One of the founding results of lattice based cryptography is a quantum reduction from the Short Integer Solution (SIS) problem to the Learning with Errors (LWE) problem introduced by Regev. It has recently been pointed out by Chen, Liu and Zhandry [CLZ22] that this reduction can be made more powerful by replacing the LWE problem with a quantum equivalent, where the errors are given in quantum superposition. In parallel, Regev’s reduction has recently been adapted in the context of code-based cryptography by Debris, Remaud and Tillich [DRT23], who showed a reduction between the Short Codeword Problem and the Decoding Problem (the DRT reduction). This motivates the study of the Quantum Decoding Problem (QDP), which is the Decoding Problem but with errors in quantum superposition and see how it behaves in the DRT reduction.

The purpose of this paper is to introduce and to lay a firm foundation for QDP. We first show QDP is likely to be easier than classical decoding, by proving that it can be solved in quantum polynomial time in a large regime of noise whereas no non-exponential quantum algorithm is known for the classical decoding problem. Then, we show that QDP can even be solved (albeit not necessarily efficiently) beyond the information theoretic Shannon limit for classical decoding. We give precisely the largest noise level where we can solve QDP giving the information theoretic limit for this new problem. Finally, we study how QDP can be used in the DRT reduction. First, we show that our algorithms can be properly used in the DRT reduction showing that our quantum algorithms for QDP beyond Shannon capacity can be used to find minimal weight codewords in a random code. On the negative side, we show that the DRT reduction cannot be, in all generality, a reduction between finding small codewords and QDP by exhibiting quantum algorithms for QDP where this reduction entirely fails. Our proof techniques include the use of specific quantum measurements, such as q-ary unambiguous state discrimination and pretty good measurements as well as strong concentration bounds on weight distribution of random shifted dual codes, which we relate using quantum Fourier analysis.

Distributed algorithms and graphs
Tuesday April 30, 2024, 3:15PM, 3052 Sophie Germain
Gianlorenzo D'Angelo (GSSI) Sparse Temporal Spanners with Low Stretch

A temporal graph is an undirected graph G = (V,E) along with a function that assigns a time-label to each edge in E. A path in G such that the traversed time-labels are non-decreasing is called a temporal path. Accordingly, the distance from u to v is the minimum number of edges of a temporal path from u to v. A temporal alfa-spanner of G is a (temporal) subgraph H that preserves the distances between any pair of vertices in V, up to a multiplicative stretch factor of alfa. The size of H is measured as the number of its edges. In this work, we study the size-stretch trade-offs of temporal spanners. In particular we show that temporal cliques always admit a temporal (2k-1)-spanner with \tilde{O}(kn^{1+1/k}) edges, where k > 1 is an integer parameter of choice and n is the number of nodes in G. Choosing k = log n, we obtain a temporal O(log n)-spanner with \tilde{O}(n) edges that has almost the same size (up to logarithmic factors) as the temporal spanner given in [Casteigts et al., JCSS 2021] to preserve temporal connectivity. We then turn our attention to general temporal graphs. Since \Omega(n^2) edges might be needed by any connectivity-preserving temporal subgraph [Axiotis et al., ICALP'16], we focus on approximating distances from a single source. We show that \tilde{O}(n/log(1+epsilon)) edges suffice to obtain a stretch of (1+epsilon), for any small epsilon > 0. This result is essentially tight in the following sense: there are temporal graphs G for which any temporal subgraph preserving exact distances from a single-source must use \Omega(n^2) edges.

Distributed algorithms and graphs
Tuesday April 30, 2024, 11AM, 1003 Sophie Germain
Alexis Baudin (LIP6) Faster maximal clique enumeration in large real-world link streams

Link streams offer a good model for representing interactions over time. They consist of links (b,e,u,v), where u and v are vertices interacting during the whole time interval [b,e]. In this talk, we deal with the problem of enumerating maximal cliques in link streams. A clique is a pair (C,[t0,t1]), where C is a set of vertices that all interact pairwise during the full interval [t0,t1]. It is maximal when neither its set of vertices nor its time interval can be increased. Some of the main works solving this problem are based on the famous Bron-Kerbosch algorithm for enumerating maximal cliques in graphs. We take this idea as a starting point to propose a new algorithm which matches the cliques of the instantaneous graphs formed by links existing at a given time to the maximal cliques of the link stream. We compute its complexity, which is better than the state-of-the art ones in many cases of interest. We also study the output-sensitive complexity, which is close to the output size, thereby showing that our algorithm is efficient. To confirm this, we perform experiments on link streams used in the state of the art, and on massive link streams, up to 100 million links. In all cases our algorithm is faster, mostly by a factor of at least 10 and up to a factor of 10^4. Moreover, it scales to massive link streams for which the existing algorithms are not able to provide the solution. For more details, please consult the following paper: https://arxiv.org/abs/2302.00360.

Non-permanent members' seminar
Thursday May 2, 2024, 4PM, Salle 3052
Ulysse Lechine Introduction to Kolmogorov complexity

In 1963 Andrey Kolmogorov came up with the definition of Kolmogorov complexity : the kolmogorov complexity of a string $w\in {0;1}^*$ noted $K(w)$ is the size of the smallest program $p$ which stops after printing $w$. In this sense it can for instance be made formal to say that 0101010101010101 is a less random/complex string than 56748195473159418. This notion of complexity is universal and robust (for instance it doesn't matter in which language the program $p$ is written), it has been studied for its own sake and is also used in number theory, combinatorics, probabilisic theory, computability theory, complexity theory (P=NP) etc… where it has led to new or simplified proofs.

We will present an introduction to Kolmogorov theory and some beautiful applications. We will also talk about a new recent result of Léchine and Seiller ( https://hal.science/hal-04539439 ) which features a very neat open combinatorics problem which you may help solve. No background is needed.

Syntax Meets Semantics
Thursday May 2, 2024, 2PM, Salle 3071
Mariana Milicich (IRIF, Universite Paris Cite) Hybrid Intersection Types for PCF

I will present a type system based on non-idempotent intersection types for PCFh, a variant of PCF. Evaluation in PCFh is hybrid: call-by-name (CBN) and call-by-value (CBV) behaviours cohabit together. Specifically, function application follows CBV semantics, while recursion has a CBN flavour. This hybrid nature is reflected in the type system, which turns out to be sound and complete with respect to PCFh evaluation. This means not only that typability implies normalisation, but also that the converse holds. Moreover, the type system is quantitative, since the size of typing derivations provides upper bounds for the length of normalisation sequences. By refining this type system, we obtain a tight type system, which offers exact information regarding the length of normalisation sequences.

Higher categories, polygraphs and homotopy
Friday May 3, 2024, 2PM, Salle 3058
Félix Loubaton (MPIM) Construction de Grothendieck lax

La construction de Grothendieck est une construction fondamentale de la théorie des catégories. Dans cet exposé, j'en donnerai une généralisation dans le cadre des $\omega$-catégories faibles. À cette fin, je présenterai quelques concepts importants de la théorie des $\omega$-catégories faibles, tels que les transformations lax, les (co)limites lax, et les fibrations cartésiennes. Enfin, j'expliquerai comment ce résultat peut être utilisé pour donner des calculs explicites d'extensions de Kan lax.

Verification
Monday May 6, 2024, 11AM, 3052 and Zoom link
Giovanni Bernardi (IRIF) To be announced.

One world numeration seminar
Tuesday May 7, 2024, 2PM, Online
Tom Kempton (University of Manchester) The Dynamics of the Fibonacci Partition Function

The Fibonacci partition function $R(n)$ counts the number of ways of representing a natural number $n$ as the sum of distinct Fibonacci numbers. For example, $R(6)=2$ since $6=5+1$ and $6=3+2+1$. An explicit formula for $R(n)$ was recently given by Chow and Slattery. In this talk we express $R(n)$ in terms of ergodic sums over an irrational rotation, which allows us to prove lots of statements about the local structure of $R(n)$.