Institut de Recherche en Informatique Fondamentale (IRIF)

CNRS

Université Paris Cité

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.

Suivez nous sur Mastodon, Twitter/X et LinkedIn :

LinkedIn Twitter/X Mastodon

7.1.2025
Nous sommes heureux d'accueillir notre nouvelle responsable financière et comptable, Chafia Dordoigne. Vous pouvez la rencontrer dans le bureau 4002.

6.1.2025
L'IRIF vous souhaite une excellente année, riche en découvertes scientifiques, en succès académiques et en épanouissement personnel !

popl_2025.jpg

26.11.2024
Félicitations aux membres de l'IRIF suivants dont les articles ont été acceptés pour la conférence POPL 2025 : Rida Ait El Manssour, Guillaume Baudart, Adrienne Lancelot, Giulio Manzonetto, Gabriel Scherer et Mahsa Shirmohammadi.

11.12.2024
Le lundi 16 décembre 2024, SOC² organise une journée dédiée aux modèles de calcul basés sur les flots de données pour célébrer l'anniversaire du célèbre article de Gilles Kahn sur les KPN, intitulé « The semantics of a simple language for parallel programming », publié en 1974. L'objectif est d'explorer les divers domaines de recherche introduits par cet article. La journée débutera par une présentation de l'article original. Le programme ainsi que le lien d'inscription (gratuit) sont disponibles ici :

csl2024.jpg

28.11.2024
Le prix Ackermann récompense des thèses exceptionnelles en logique informatique lors de la conférence ACSL. Cette année, le prix a été attribué à deux thèses encadrées à l'IRIF : les lauréats sont Gaëtan Douéneau-Tabot, encadré par Olivier Carton et Emmanuel Filiot à l'Université Paris-Cité (France), et Aliaume Lopez, encadré par Jean Goubault-Larrecq et Sylvain Schmitz à l'ENS Paris-Saclay et à l'Université Paris-Cité (France), respectivement. Ils recevront leur prix à CSL 2025, à Amsterdam, qui aura lieu du 10 au 14 février 2025.


(Ces actualités sont présentées selon un classement mêlant priorité et aléatoire.)

Algorithmes et complexité
Mardi 21 janvier 2025, 11 heures, Salle 3052
Jérémie Roland (ULB, Brussels) Eigenpath traversal by Poisson-distributed phase randomisation

We present a framework for quantum computation, similar to Adiabatic Quantum Computation (AQC), that is based on the quantum Zeno effect. By performing randomised dephasing operations at intervals determined by a Poisson process, we are able to track the eigenspace associated to a particular eigenvalue. We derive a simple differential equation for the fidelity leading to general theorems bounding the time complexity of a whole class of algorithms. We also use eigenstate filtering to optimise the scaling of the complexity in the error tolerance $ε$. In many cases the bounds given by our general theorems are optimal, giving a time complexity of $O(1/Δ)$ with $Δ$ the minimum of the gap. This allows us to prove optimal results using very general features of problems, minimising the amount of problem-specific insight necessary. As two applications of our framework we obtain optimal scaling for the Grover problem (i.e. $O(N^{1/2})$ where $N$ is the database size) and the Quantum Linear System Problem (i.e. $O(κ \log(1/ε))$ where $κ$ is the condition number and $ε$ the error tolerance) by direct applications of our theorems.

Joint work with Joseph Cunningham.

Algorithmique distribuée et graphes
Mardi 21 janvier 2025, 11 heures, 1014
Hugo Jacob (LIRMM, Montpellier) On the structure of twin-width 1 graphs

We investigate the structure of graphs of twin-width at most 1 and uncover nice relations with several classical classes of hereditary graphs. An important finding is that they are permutation graphs and that their permutation diagrams and contraction sequences are closely related. We use these combinatorial tools to establish a recursive decomposition theorem for twin-width 1 graphs, and deduce a simple recognition algorithm running in linear time.

Joint work with Jungho Ahn, Noleen Köhler, Christophe Paul, Amadeus Reinald, and Sebastian Wiederrecht.

One world numeration seminar
Mardi 21 janvier 2025, 14 heures, Online
Thomas Garrity (Williams College) Multi-dimensional continued fractions and integer partitions: Using the Natural Extension to create a tree structure on partitions

The goal is to explore the recently found interplay between integer partitions and the dynamics of the triangle map (a type of multi-dimensional continued fraction algorithm). (This is joint work with Baalbaki, Bonanno, Del Vigna and Isola.)

As we will see, the triangle map gives an almost internal symmetry from the set of integer partitions to itself, which in turn allows the generation of any number of new partition identities.

Further, this allows us to place a tree structure on the space of all integer partitions. (This is joint work with Joe Fox and with Jacob Lehmann Duke). This tree structure allowed us to find the natural extension of the triangle map in any dimension. As with the classical Farey map, the dynamics of this map, in every dimension, has an indifferent fixed point, which in turn can be used to understand the structure of the integer partition tree.

Among the many different types of multi-dimensional continued fractions that exist, for still unknown reasons it appears that the triangle map is the only one that is “partition” compatible.

Thus we use the triangle map (stemming from number theory and dynamics) to understand classical integer partition numbers from combinatorics, and use partition numbers to understand the dynamics of the triangle map.

Preuves, programmes et systèmes
Jeudi 23 janvier 2025, 10 heures, Amphithéâtre Alan Turing du bâtiment Sophie Germain
Nathanaëlle Courant (INRIA Paris and OCamlPro) An efficient and verified convertibility check in dependent type theory

The convertibility test, which checks if two λ-terms are equal up to β-reduction, is an essential part of typechecking and proof verification in proofs assistants based on type theory, such as Coq, Agda and Lean. Naturally, the correctness of such a test is necessary to ensure the proofs thus verified are valid; but having an efficient test is also required both for real-time interaction with the user, and for proof search.

In this presentation, we start with an efficient, strong call-by-need, big-step semantics for the λ-calculus, which is the critical building block to implement a convertibility test in a classical manner. We then show how we can improve upon this by considering the convertibility problem in its entirety, viewing it as proof search. To this end, we study what can be considered a (non-)convertibility proof, drawing upon existing work.

This gives rise to a new parallel, heuristic-less algorithm for this test, which does not duplicate computations, and comes with worst-case complexity guarantees. We derived a virtual machine from this algorithm, and made it more efficient by following Grégoire and Leroy, showing that our algorithm is suited to compilation of the input λ-terms for additional efficiency. Both this semantics and this efficient parallel convertibility test have been implemented in OCaml and experimentally validated, significantly outperforming Coq in some cases. They are also both formalised and verified using Coq, building confidence in our work.

Séminaire des membres non-permanents
Jeudi 23 janvier 2025, 16 heures, Salle 3052
Miriam Marzaioli Non encore annoncé.

La syntaxe rencontre la sémantique
Jeudi 23 janvier 2025, 13 heures 30, Salle 3052
Gabriele Tedeschi (Univ. Pisa) Modelling Quantum Protocols: a Novel Semantics with Quantum Probabilities

Quantum protocols involve a number of features like concurrent execution, quantum primitives, message communication and non-determinism. The well-studied calculi and models for probabilistic concurrent systems seem inadequate in the quantum setting, as they do not comply with the observational limitations of quantum theory. We will explore a new semantic model made of “Quantum Distributions” and “Quantum Transition Systems”, instead of probability distributions and probabilistic LTSs. We provide a symbolic, quantum semantics for a minimal quantum process calculus, which we prove sound and complete with respect to the known ground, probabilistic behaviour of quantum processes.

Automates
Vendredi 24 janvier 2025, 14 heures, Salle 3052
Olivier Carton (IRIF) Rauzy dimension and finite state dimension

In a paper of 1976, Rauzy studied two complexity notions, $\underline{β}$ and $\overline{β}$, for infinite sequences over a finite alphabet. The function $\underline{β}$ is maximum exactly in the Borel normal sequences and $\overline{β}$ is minimum exactly in the sequences that, when added to any Borel normal sequence, the result is also Borel normal. Although the definition of $\underline{β}$ and $\overline{β}$ do not involve finite-state automata, we establish some connections between them and the lower $\underline{\dim}$ and upper $\overline{\dim}$ finite-state dimension (or other equivalent notions like finite-state compression ratio, entropy or cumulative log-loss of finite-state predictors). We show tight lower and upper bounds on $\underline{\dim}$ and $\overline{\dim}$ as functions of $\underline{β}$ and $\overline{β}$, respectively. In particular this implies that sequences with $\overline{\dim}$ zero are exactly the ones that that, when added to any Borel normal sequence, the result is also Borel normal. We also show that the finite-state dimensions $\underline{\dim}$ and~$\overline{\dim}$ are essentially subadditive.

Vérification
Lundi 27 janvier 2025, 11 heures, Salle 3052
Enrico Bini (University of Turin) Cutting the Unnecessary Deadlines in EDF

Together with Fixed Priority Scheduling, Earliest Deadline First (EDF) is the second leg on top of which a large portion of the research on real-time systems stands. At the heart of the EDF exact schedulability test, a pivotal role is played by the demand bound function test, which requires to evaluate whether the amount of work required to complete a set of jobs is less than or equal to the amount of time available. Such a test is checked over a set of time instants.

In this work, it is proposed a method that cuts drastically the set of constraints to be checked. Such a method is applicable also to tasks with release offset. Notably, it is proved that such a reduced set of constraints is minimal: it is not possible to reduce the set any further without losing the sufficiency of the test. The code to make this reduction is publicly available on GitHub.

Programmation
Lundi 27 janvier 2025, 10 heures, IRIF
Jules Viennot (IRIF) Implementation of purely functional catenable double-ended queue

Twenty-five years ago, Kaplan and Tarjan established a striking result: there exist “purely functional, real-time deques with catenation”. In other words, there exists a data structure that supports the following operations: “push” and “pop” which insert and extract one element at the front end, “inject” and “eject” which insert and extract one element at the rear end and “concat”, the concatenation operation. Moreover, the data structure is persistent: none of the five operations modifies or destroys its argument. Finally, each operation has worst-case time complexity O(1). This presentation will provide an overview of the first ever implementation of the data structure, done in OCaml, and its verification in Rocq.

Algorithmique distribuée et graphes
Mardi 28 janvier 2025, 15 heures, 3052
Gil Puig I Surroca (Université Paris Dauphine) Endomorphism monoids of regular graphs

Back in 1939, Frucht proved that every finite group is isomorphic to the automorphism group of a finite graph. This incited an examination of the influence that standard graph theoretical concepts can have on automorphism groups. Eventually, the framework was enlarged by extending the analyses to endomorphism monoids. This has ultimately established a particular connection between semigroup classes and graph classes, notably in terms of sparsity and combinatorial regularity. The goal of the presentation is to contextualize a new result on endomorphism monoids of regular graphs that adds some detail to the picture. This is joint work with Kolja Knauer.