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

podcastrechercheclairemathieufc.jpg

19.3.2024
Après avoir été augmenté en septembre 2023, le budget alloué à l’Enseignement supérieur et à la Recherche est finalement réduit de 904 millions d’euros. Le podcast “La Science, CQFD” de France Culture s'est demandé comment se porte la recherche française et quelle direction elle prend. Claire Mathieu, directrice de recherche au CNRS à l'IRIF, intervient.

27.3.2024
Nous accueillons une nouvelle directrice de recherche à l'IRIF, Tayssir Touilli. Ses domaines d'intérêt sont la détection de logiciels malveillants, la vérification de logiciels et les méthodes formelles. Vous pouvez la rencontrer dans le bureau 4028A.

quentin_aristote.jpg

29.3.2024
Bravo à Quentin Aristote, doctorant, qui a reçu le prix Helena Rasiowa pour le meilleur papier étudiant, lors de la 32ème conférence EACSL : Active Learning of Deterministic Transducers with Outputs in Arbitrary Monoids.

15.3.2024
La deuxième conférence “On éteint, on réfléchit, on discute”, organisée à l'Université Paris Cité par François Laroussinie, portera sur “Les communs numériques”. Serge Abiteboul et Valérie Peugeot sont les conférenciers invités. Elle se tiendra le 19 mars 2024, de 16h à 18h. Cet événement est gratuit.

mirna-dzamonja.jpeg

28.3.2024
La Société mathématique de Belgique (SMB) a décerné à Mirna Džamonja (CNRS, IRIF, Université de Paris) le “Prix Godeaux” de la SMB. “Ce prix est décerné chaque année, sur proposition d'un membre du conseil d'administration de la BMS, à un-e mathématicien-ne belge ou international-e de renom qui est invité-e à donner une conférence en Belgique”. Toutes nos félicitations !

marie-jose_iarifina.jpg

27.3.2024
Marie-Josée Iarifina a rejoint l'IRIF pour remplacer Natalia Hacquart en tant que gestionnaire financière et comptable. Venez la rencontrer et lui souhaiter la bienvenue dans le bureau 4002.

12.3.2024
Hugo Herbelin, directeur de recherche Inria à l'IRIF, organise la prochaine journée Horizon Maths sur le sujet : Preuve mathématique et sûreté logicielle. Elle aura lieu le mercredi 27 mars 2024 de 9h à 18h à l'institut Henri Poincaré (5 rue Pierre et Marie Curie, Paris 5e), amphithéâtre Hermite. Inscription gratuite mais obligatoire :

30.1.2024
Comment concevoir des algorithmes pour analyser les protocoles de vote électronique ? Comment définir mathématiquement le secret du vote ? Quels sont les enjeux ? Retrouvez l'interview que Véronique Cortier nous a accordée avant sa conférence du 7 février 2024.


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

Preuves, programmes et systèmes
Jeudi 28 mars 2024, 11 heures, Salle 3052
Fabio Gadducci (University of Pisa) On Petri nets and monoidal categories (with a bit of linear logic)

A classical result in concurrency theory shows that an algebraic interpretation of Petri nets in terms of commutative monoids can be used to provide a characterisation of the deterministic computations of a net via monoidal categories, accounting for their sequential and parallel composition. In turn, this characterisation leads to the interpretation of such computations as sequents of the multiplicative fragment of linear logic. The talk presents a survey of the topic, including recent results concerning non-deterministic computations and their characterisation in terms of dioidal categories, the categorical equivalent of tropical semirings, as well as suggesting a possible connection with the multiplicative additive fragment of linear logic.

Séminaire des membres non-permanents
Jeudi 28 mars 2024, 16 heures, Salle 3052 and Zoom link
Arturo De Faveri A gentle introduction to universal algebra

Universal algebra concerns the study of those mathematical objects that behave like 'algebraic structures' (i.e. groups, rings, vector spaces…). This talk is divided into two parts. In the first we try to understand what 'algebraic structures' have in common, offering an overview of the basic concepts of universal algebra. In the second we survey some selected topics that link universal algebra with logic and computer science.

La syntaxe rencontre la sémantique
Jeudi 28 mars 2024, 14 heures, Salle 3052
Noam Zeilberger (LIX, Polytechnique) An introduction to type refinement systems

I will give an introduction to type refinement systems in the style of Frank Pfenning et al., discuss the phenomenon of how refinement typing makes some aspects of evaluation order visible in the type system, and give some general indications of how type refinement may be understood from a categorical perspective. For background reading, you can see my notes from OPLSS 2016 on “Principles of type refinement” (https://noamz.org/oplss16/refinements-notes.pdf).

Automates
Vendredi 29 mars 2024, 14 heures, Salle 3052
Leonid Libkin Embedded finite models and finitely representable databases: a forgotten area ready for a comeback

A question was asked 35 years: can we store an infinite set in a database? Turns out the answer is yes, and for this a set has to be finitely representable. In databases we use logic for querying, and thus finitely represent sets by logical formulas over infinite models. The next question was: what can you ask about such databases? To answer this question we had to go back to the finite world, and thus embedded finite models were born, a mix of finite and the infinite. While theoreticians were happy to talk about AC0 and o-minimality, cell decomposition, and local triviality in the same paper, practitioners asked whether something useful can be built based on these ideas. The 1990s answer was no, computers were too slow, solvers were too immature. But the world doesn’t stand still, and we have witnessed signs of rebirth of this area that at the very least gave us theoreticians lots of fun. In the talk I’ll tell this story and share some thoughts on making finitely representable databases great again.

La théorie des types et la théorie de l'homotopie
Vendredi 29 mars 2024, 15 heures 30, Salle 3052
Moana Jubert Sémantique de la théorie homotopique des types

Combinatoire énumérative et analytique
Mardi 2 avril 2024, 11 heures, Salle 3058
Relâche Séminaire Flajolet le 4 avril

Algorithmes et complexité
Mardi 2 avril 2024, 11 heures, Salle 3071
Michael Klooß (Aalto University) Adaptive Special Soundness: Improved Knowledge Extraction by Adaptive Useful Challenge Sampling

Proving knowledge soundness of an interactive proof from scratch is often a challenging task. This has motivated the development of various special soundness frameworks which, in a nutshell, separate knowledge extractors into two parts: (1) an extractor to produce a set of accepting transcripts conforming to some structure; (2) a witness recovery algorithm to recover a witness from a set of transcripts with said structure. These frameworks take care of (1), so it suffices for a protocol designer to specify (2) which is often simple®.

However, special soundness fails to adequately capture guarantees provided by simple “probabilistic tests”, e.g., short random linear combinations as used in many lattice-based proof systems. In this talk, I will introduce (adaptive) special soundness, which captures many scenarios and discuss the rewinding-based knowledge extraction. Moreover, I will point out current limitations and open problems with regard to (adaptive) special soundness.

This talk is based on join work with Thomas Attema, Russell W. F. Lai, and Pavlo Yatsyna.

Sémantique
Mercredi 3 avril 2024, 10 heures 45, Salle 3052
Thomas Nowak (LMF) Topological Characterization of Task Solvability in General Models of Computation

The famous asynchronous computability theorem (ACT) relates the existence of an asynchronous wait-free shared memory protocol for solving a task with the existence of a simplicial map from a subdivision of the simplicial complex representing the inputs to the simplicial complex representing the allowable outputs. The original theorem relies on a correspondence between protocols and simplicial maps in round-structured models of computation that induce a compact topology. This correspondence, however, is far from obvious for computation models that induce a non-compact topology, and indeed previous attempts to extend the ACT have failed. This paper shows that in every non-compact model, protocols solving tasks correspond to simplicial maps that need to be continuous. It first proves a generalized ACT for sub-IIS models, some of which are non-compact, and applies it to the set agreement task. Then it proves that in general models too, protocols are simplicial maps that need to be continuous, hence showing that the topological approach is universal. Finally, it shows that the approach used in ACT that equates protocols and simplicial complexes actually works for every compact model. Our study combines, for the first time, combinatorial and point-set topological aspects of the executions admitted by the computation model.

Joint work with Hagit Attiya and Armando Castañeda.

Catégories supérieures, polygraphes et homotopie
Vendredi 5 avril 2024, 14 heures, Salle 3058
Yonatan Harpaz Lax limits of model categories

In higher category theory, model categories constitute a powerful manner to encode infinity categories. Unfortunately, it is not always possible to encode an infinity category using a model category, and when this is possible the choice of model category is far from being unique or canonical. Favoring such presentations whenever possible, it is hence natural to investigate which operations on the level of infinity categories can be performed on the model categorical level. In this talk I will describe one such result for the operation of lax limits, showing that, under suitable conditions, if a diagram of inifinity categories is modeled by a diagram of (simplicial combinatorial) model categories, then the lax limit can be performed on the level of model categories. We also obtain results concerning homotopy limits and various intermediate limits. This generalizes previous results of Lurie and of Bergner. Related results were also obtained independently by Balzin.

Algorithmes et complexité
Vendredi 5 avril 2024, 11 heures, Salle 3052
Yanlin Chen (CWI Amsterdam) A Quantum Speed-Up for Approximating the Top Eigenvectors of a Matrix

Finding a good approximation of the top eigenvector of a given d × d matrix A is a basic and important computational problem, with many applications. We give two different quantum algorithms that, given query access to the entries of A and assuming a constant eigenvalue gap, output a classical description of a good approximation of the top eigenvector: one algorithm with time complexity d^{1.5+o(1)} and one with time complexity \tilde{O}(d^{1.75}) that has a slightly better dependence on the precision of the approximation. Both provide a polynomial speed-up over the best-possible classical algorithm, which needs Ω(d^2) queries to entries of A (and hence Ω(d^2) time). We extend this to a quantum algorithm that outputs a classical description of the subspace spanned by the top-q eigenvectors in time qd^{1.5+o(1)}. We also prove a nearly-optimal lower bound of \tilde{Ω}(d^{1.5}) on the quantum query complexity of approximating the top eigenvector. Our quantum algorithms run a version of the classical power method that is robust to certain benign kinds of errors, where we implement each matrix-vector multiplication with small and well-behaved error on a quantum computer, in different ways for the two algorithms.

Our first algorithm used block-encoding techniques to compute the matrix-vector product as a quantum state, from which we obtain a classical description by a new time-efficient unbiased pure-state tomography algorithm that has essentially optimal sample complexity O(d log(d)/ε^2) and that comes with improved statistical properties compared to earlier pure-state tomography algorithms. Our second algorithm estimated the matrix-vector product one entry at a time, using a new “Gaussian phase estimation” procedure. We also develop a time-efficient process- tomography algorithm for reflections around bounded-rank subspaces, providing the basis for our top-eigensubspace estimation application.

This is the joint work with Ronald de Wolf and András Gilyén.