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

30.5.2024
La 14ème journée francilienne de programmation se déroulera le lundi 10 juin 2024 à l'Université Paris Cité, UFR d'informatique. Cette journée est l'occasion d'une confrontation ludique et amicale entre équipes d'étudiants de licence d'informatique venues de l'université Paris Saclay, de l'université Paris Cité et de Sorbonne Université. Cette journée est organisée conjointement par Pierre Letouzey (IRIF), Jean-Baptiste Yunès (UPC), Emmanuel Chailloux (UPMC) et Jean-Christophe Filliâtre (Paris Saclay).

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 !

30.5.2024
Un poste de gestionnaire administratif-ve et financier-ère est à pourvoir ! Vous souhaitez intégrer une équipe sympathique et vous aimez le chocolat ? Ce poste est fait pour vous !

30.5.2024
Un poste d'Ingénieur de recherche en développement logiciel est à pourvoir. N'hésitez pas à partager cette offre de poste autour de vous !

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.

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 !


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

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 k-Linkage on Temporal Graphs

Given a graph \( G \) and a set of \( k \) pairs of vertices, the \( k \)-Linkage Problem asks whether there exists a set of \( k \) paths such that each path connects a given pair of vertices, and each vertex in the graph is used by at most one of these paths. When one consider temporal graphs, where the graph's structure can change over time, the \( k \)-Linkage Problem takes on new variations. This seminar focuses on a specific version where we seek time-respecting paths that connect the given pairs of vertices, ensuring that at any given time, each vertex is occupied by at most one path. I will present results on the parameterized complexity of this problem when \( k \) is given as a parameter.

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.

Automates
Vendredi 7 juin 2024, 14 heures, Salle 3052
Lê Thành Dũng (Tito) Nguyễn Computing the polynomial degree of size-to-height increase for macro tree transducers

In a paper to appear at ICALP'24 [*], Gallot, Maneth, Nakano and Peyrat show that, given a tree-to-tree function f computed by a macro tree transducer (a natural register-based machine model, which will be recalled in the talk), the following problems are decidable: (1) is height(f(t)) = O(height(t)) ? (2) is height(f(t)) = O(size(t)) ? We sketch a tentative proof of a generalization of (2) by different and arguably simpler means. More precisely, we show that the quantity inf {k | height(f(t)) = O(size(t)^k)} ∈ ℕ∪{+∞} is computable by reduction to ambiguity of (ordinary) tree automata. (Joint work with Paul Gallot and Nathan Lhote, in preparation.) [*] https://arxiv.org/abs/2307.16500

Algorithmes et complexité
Mardi 11 juin 2024, 11 heures, Salle 3052
Divyarthi Mohan (Tel-Aviv University) Optimal Stopping with Interdependent Values

Consider the problem of selling a single item to one of n buyers arriving sequentially, whereupon the arrival of each buyer we need to decide whether to accept this value and stop the process (before seeing the values of the future bidders), or irrevocably and irreversibly reject this bidder and continue on to the next. The objective is to maximize the accepted value, which poses a fundamental question: how effectively can an online algorithm perform compared to the offline optimal solution? Further, adding to the challenge in many scenarios a bidder's value for the item may depend on private information of other bidders. For example, in an art auction, a buyer's value for the item may be influenced by how other buyer's so far have liked it, and in fact, may even depend on how the future buyers will value the item as that would affect its resale value.

We study online selection problems in both the prophet and secretary settings, when arriving agents have interdependent values. In the interdependent values model, introduced in the seminal work of Milgrom and Weber [1982], each agent has a private signal and the value of an agent is a function of the signals held by all agents. Results in online selection crucially rely on some degree of independence of values, which is conceptually at odds with the interdependent values model. For prophet and secretary models under the standard independent values assumption, prior works provide constant factor approximations to the welfare. On the other hand, when agents have interdependent values, prior works in Economics and Computer Science provide truthful mechanisms that obtain optimal and approximately optimal welfare under certain assumptions on the valuation functions. We bring together these two important lines of work and provide the first constant factor approximations for prophet and secretary problems with interdependent values. We consider both the algorithmic setting, where agents are non-strategic (but have interdependent values), and the mechanism design setting with strategic agents. All our results are constructive and use simple stopping rules.

Joint work with Simon Mauras and Rebecca Reiffenhäuser.