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

perso-ahmed-bouajjani.jpg

27.5.2024
Ahmed Bouajjani, Professeur à l'IRIF, a été récompensé pour sa contribution à la recherche dans le domaine de l'informatique. Il a été nominé dans la catégorie Recherche scientifique pour la 6ème édition des Trophées Marocains du Monde. Toutes nos félicitations !

dts_omer_reingold.jpg

10.4.2024
L'IRIF a le plaisir d'annoncer son deuxième Distinguished Talk de l'année ! Notre conférencier invité est Omer Reingold, professeur d'informatique à l'université de Stanford et directeur de la Simons Collaboration sur la théorie de l'Équité algorithmique (Simons Foundation). Il parlera de l'équité algorithmique. Toute personne intéressée est invitée à se joindre à nous pour cette conférence !

12.4.2024
La rediffusion de la conférence (en anglais) de Véronique Cortier, qui s'est tenue en février, est désormais disponible sur la chaîne YouTube de l'IRIF. Son sujet était : “Le vote électronique : conception et vérification formelle”.

logopintofscience2024.jpg

10.4.2024
Trois projets de médiation scientifique de chercheurs à l'IRIF ont été sélectionnés pour l'édition 2024 de Pint of Science France-Paris. Le principe : découvrir une thématique ou un sujet scientifique, dans un bar. Nos chercheurs parleront protection des données, graphes et informatique quantique.


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

Algorithmes et complexité
Mercredi 29 mai 2024, 14 heures, Salle 3052
Leo Zhou (Caltech) Local Minima in Quantum Systems

Finding ground states of quantum many-body systems is known to be hard for both classical and quantum computers. As a result, when Nature cools a quantum system in a low-temperature thermal bath, the ground state cannot always be found efficiently. Instead, Nature finds a local minimum of the energy. In this work, we study the problem of finding local minima in quantum systems under thermal perturbations. While local minima are much easier to find than ground states, we show that finding a local minimum is computationally hard for classical computers, even when the task is to output a single-qubit observable at any local minimum. In contrast, we prove that a quantum computer can always find a local minimum efficiently using a thermal gradient descent algorithm that mimics the cooling process in Nature. To establish the classical hardness of finding local minima, we consider a family of two-dimensional Hamiltonians such that any problem solvable by polynomial-time quantum algorithms can be reduced to finding local minima of these Hamiltonians. Therefore, cooling systems to local minima is universal for quantum computation, and, assuming quantum computation is more powerful than classical computation, finding local minima is classically hard and quantumly easy.

Séminaire des membres non-permanents
Jeudi 30 mai 2024, 16 heures, Salle 3052
Victor Arrial The Bang-Calculus: An Accessible Introduction to Subsuming Paradigms

The lambda calculus is a formal system that serves as the foundation for functional programming languages. It supports different evaluation strategies, resembling the evaluation processes of various programming languages such as Haskell and OCaml. The Bang Calculus is an extension of the lambda calculus introduced to provide explicit counterparts for these strategies, thus allowing a uniform study of them.

In this talk, we will present the Bang Calculus and provide multiple examples of (simple) properties that can be subsumed within this framework. Absolutely no prerequisites are required.

Catégories supérieures, polygraphes et homotopie
Vendredi 31 mai 2024, 14 heures, Salle 3058
Sacha Ikonicoff Catégories différentielles et tangentes pour les algèbres sur une opérade

La notion de catégorie différentielle cartésienne permet de formaliser dans un contexte catégorique la notion de dérivée directionnelle. Similairement, la notion de catégorie tangente fournit un analogue à la notion de fibré tangent de la géométrie différentielle dans le contexte de la théorie des catégories.
  Dans cet exposé, nous décrirons une nouvelle notion de monade différentielle cartésienne. Cette structure consiste en une monade équipée d'une transformation naturelle appelée "combinateur différentiel". Pour une telle monade, nous montrerons que la catégorie (opposée) de Kleisli associée est munie d'une structure différentielle cartésienne, et que la catégorie d'algèbres associée est munie d'une structure tangente.
  Finalement, nous considérerons l'exemple des algèbres sur une opérade. Nous montrerons que la monade associée à toute opérade (algébrique, symétrique) admet un combinateur différentiel. Nous étudierons la catégorie différentielle cartésienne et la catégorie tangente associée. Nous montrerons que cette catégorie tangente admet une structure tangente adjointe qui permet de retrouver certaines notions provenant de la géométrie algébrique et non-commutative.

Automates
Vendredi 31 mai 2024, 14 heures, Salle 3052
Thomas Colcombet Bisimulation invariant MSO over finite transition systems

In this talk, I will present a recent result obtained in collaboration with Amina Doumane and Denis Kuperberg on the properties definable in MSO which are bisimulation invariant over finite transition systems. We show that these coincide with mu-calculus-definable properties. This is a variant of a result from Janin and Walukiewicz over general (ie possibly infinite) transition systems [JW96].

Our proof techniques involve developing an algebraic theory of infinite regular trees, in particular establishing on the way that recognizable languages of regular trees coincide (over regular trees) with MSO definable language of trees.

Graph Transformation Theory and Applications
Vendredi 31 mai 2024, 15 heures, online
Kristopher Brown (Topos Institute, Berkeley, California, USA) A graphical language for programming with graph rewriting

We provide a general introduction to the AlgebraicJulia ecosystem and AlgebraicRewriting.jl, which allows for integrating general-purpose code with computation of many graph transformation constructions in a broad variety of categories. Practical applications of graph transformation depend on being able to apply sequences of rewrites in a controlled manner: we present work on a graphical language for the construction and composition of such programs, including computation of normal forms as well as scientific agent-based model simulations. This graphical language can be given semantics in many different contexts (e.g. deterministic, nondeterministic, probabilistic) and can be functorially migrated, which yields graph rewriting programs that operate in other categories.

Zoom meeting registration link

YouTube live stream

Combinatoire énumérative et analytique
Mardi 4 juin 2024, 11 heures, Salle 1007
Pas De Séminaire (Mais Séminaire Flajolet Le Jeudi 6 Juin !) Pas de séminaire

Algorithmes et complexité
Mardi 4 juin 2024, 11 heures, Salle 3052
Kuo-Chin Chen (Foxconn Research) Quantum Walks on Simplicial Complexes and Harmonic Homology: Application to Topological Data Analysis with Superpolynomial Speedups

Incorporating higher-order interactions in information processing enables us to build more accurate models, gain deeper insights into complex systems, and address real-world challenges more effectively. However, existing methods, such as random walks on oriented simplices and homology, which capture these interactions, are not known to be efficient. This work investigates whether quantum walks on simplicial complexes exhibit quantum advantages. We introduce a novel quantum walk that encodes the combinatorial Laplacian, a key mathematical object whose spectral properties reflect the topology of the underlying simplicial complex. Furthermore, we construct a unitary encoding that projects onto the kernel of the Laplacian, representing the space of harmonic cycles in the complex's homology. Combined with the efficient construction of quantum walk unitaries for clique complexes that we present, this paves the way for utilizing quantum walks to explore higher-order interactions within topological structures. Our results achieve superpolynomial quantum speedup with quantum walks without relying on quantum oracles for large datasets.

Crucially, the walk operates on a state space encompassing both positively and negatively oriented simplices, effectively doubling its size compared to unoriented approaches. Through coherent interference of these paired simplices, we are able to successfully encode the combinatorial Laplacian, which would otherwise be impossible. This observation constitutes our major technical contribution. We also extend the framework by constructing variant quantum walks. These variants enable us to: (1) estimate the normalized persistent Betti numbers, capturing topological information throughout a deformation process, and (2) verify a specific QMA1-hard problem, showcasing potential applications in computational complexity theory.

Algorithmes et complexité
Mercredi 5 juin 2024, 11 heures, Salle 4052 (PCQC)
Marin Costes (Université Paris-Saclay) Space-time deterministic graph rewriting

We study non-terminating graph rewriting models, whose local rules are applied non-deterministically—and yet enjoy a strong form of determinism, namely space-time determinism. Of course in the case of terminating computation it is well-known that the mess introduced by asynchronous rule applications may not matter to the end result, as confluence conspires to produce a unique normal form. In the context of non-terminating computation however, confluence is a very weak property, and (almost) synchronous rule applications is always preferred e.g. when it comes to simulating dynamical systems. Here we provide sufficient conditions so that asynchronous local rule applications conspire to produce well-determined events in the space-time unfolding of the graph, regardless of their application orders. Our first example is an asynchronous simulation of a dynamical system. Our second example features time dilation, in the spirit of general relativity.

Séminaire des membres non-permanents
Jeudi 6 juin 2024, 16 heures, Salle 3052
Allen Ibiapina Non encore annoncé.

La syntaxe rencontre la sémantique
Jeudi 6 juin 2024, 14 heures, Salle 3071
Adrienne Lancelot (LIX Polytechnique and IRIF UPC) Mirroring Call-by-Need, or Values Acting Silly

Call-by-need evaluation for the lambda-calculus can be seen as merging the best of call-by-name and call-by-value, namely the wise erasing behaviour of the former and the wise duplicating behaviour of the latter. To better understand how duplication and erasure can be combined, we design a degenerated calculus, dubbed call-by-silly, that is symmetric to call-by-need in that it merges the worst of call-by-name and call-by-value, namely silly duplications by-name and silly erasures by-value.

We validate the design of the call-by-silly calculus via rewriting properties and multi types. In particular, we mirror the main theorem about call-by-need – that is, its operational equivalence with call-by-name – showing that call-by-silly and call-by-value induce the same contextual equivalence. This fact shows the blindness with respect to efficiency of call-by-value contextual equivalence. We also define a call-by-silly strategy and measure its length via tight multi types. Lastly, we prove that the call-by-silly strategy computes evaluation sequences of maximal length in the calculus.