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

24.10.2024
L'informatique a-t-elle un avenir ? Telle est la question qui sera débattue lors de la troisième conférence “On éteint, on réfléchit, on discute”, organisée à l'Université Paris Cité par François Laroussinie. José Halloy (LIED) et Anne-Laure Ligozat (LISN) sont les conférenciers invités. Elle se tiendra le mardi 10 décembre 2024, de 16h15 à 18h30. Cet événement est gratuit.

pp_dexterkozen.jpg

31.10.2024
L’IRIF est ravi d’accueillir Dexter Kozen de l’Université Cornell en tant qu'intervenant de nos Distinguished Talks. La conférence aura lieu le 3 décembre 2024 à partir de 11h. Plus de détails à venir !

5.11.2024
Cette année, trois chercheurs de l'IRIF font partie de deux projets ayant été retenus pour une bourse Synergie 2025 du Conseil Européen de la Recherche (ERC). Toutes nos félicitations à Valérie Berthé, Hugo Herbelin et Paul-André Melliès ! Nous leur souhaitons d'obtenir des résultats concluants.

perso-sergio-rajsbaum.jpg

24.10.2024
Le prix de l'Innovation a été décerné à Sergio Rajsbaum, membre associé de l'IRIF, dans le cadre de son importante contribution à l'Informatique Distribuée. Ce prix lui sera remis lors de la conférence SIROCCO'25 à Delphes, en Grèce.

pp_melissa_godde.jpg

18.10.2024
Nous souhaitons la bienvenue à Mélissa Goddé, nouvelle gestionnaire, qui vient renforcer l'équipe administrative.

optimisation_web.jpg

25.9.2024
CNRS Sciences Informatiques organise la conférence « L'optimisation : au cœur des défis de l'informatique » qui aura lieu le 3 octobre 2024, au siège du CNRS. Cet événement, destiné aux professionnels de l'industrie, aux décideurs et aux journalistes, rassemble la communauté scientifique pour échanger et partager les connaissances sur ce sujet transdisciplinaire. Claire Mathieu, Simon Apers et David Saulpic y interviendront.

formatsbestpaperaward2024.jpg

18.9.2024
Neha Rino (stagiaire MPRI à l'IRIF en 2023), Eugène Asarin et Mohammed Foughali ont remporté le Best Paper Award à FORMATS. Ce travail formule et résout par un algorithme efficace le problème du suivi quantitatif : calculer un nombre réel caractérisant dans quelle mesure la trace donnée d'un système temps réel satisfait sa spécification.

jlkrivine_lesdecompilateurs.jpg

30.9.2024
Jean-Louis Krivine, professeur émérite à l'IRIF, a publié un livre, “Les décompilateurs - L'Univers en tête”. Vous y trouverez, entre autres, une réflexion sur l'origine des mathématiques et le lien entre logique et informatique théorique ainsi que quelques paradoxes en mécanique quantique.


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

Automates
Vendredi 8 novembre 2024, 14 heures, Salle 3071
Benjamin Bordais (TU Dortmund) How to generalize turn-based games into well-behaving concurrent games

We investigate two-player win/lose games over finite graphs. In all generality, these games are concurrent, i.e. at each state of the graph, there is a concurrent interaction between the two players to determine the next state visited. In the special case where, at every state of the graph, there are no real concurrent interaction, i.e. only one player is truly playing, the game is turn-based. Various desirable properties hold on turn-based games, but do not on arbitrary concurrent games; e.g. there exist subgame optimal strategies in all prefix-independent turn-based games, while there do not in very simple prefix-independent concurrent games. A possible way to circumvent this issue is to define a subclass of concurrent games, that is a proper superclass of turn-based games, while enjoying several of their nice properties. The goal of this talk is to introduce such a subclass of concurrent games, namely finitely maximizable games, and to show step by step how we came up with this definition. The novel way that we use to define such a subclass of well-behaving concurrent games constitutes a promising approach for investigating more general concurrent games, such as non-antagonistic two-player games, or even multi-player games.

La théorie des types et la théorie de l'homotopie
Vendredi 8 novembre 2024, 14 heures, Salle 1013
Sylvain Douteau Remarques sur le modèle simplicial de l’univalence, d’après Kapulkin-Lumsdaine-Voevodsky (II)

Combinatoire énumérative et analytique
Mardi 12 novembre 2024, 11 heures, Salle 3071
Relâche relâche

Algorithmique distribuée et graphes
Mardi 12 novembre 2024, 15 heures, 3052
Students Presenting At Jga (IRIF and LIP6) JGA training seminar

Presentations given by students who will be presenting at JGA 2024.

Hector Buffière: Shallow vertex minors, stability, and dependence (abstract: https://jga2024.sciencesconf.org/579556)

Renaud Torfs: Biclique maximum des graphes Star_1,2,3-free sans jumeau et des graphes de bimodularwidth bornée (abstract: https://jga2024.sciencesconf.org/579711)

Guillaume Aubian: Une construction de graphes de grand nombre chromatique sans triangle (abstract: https://jga2024.sciencesconf.org/581565)

Jules Bouton Popper: Comment rendre un graphe temporel connecté ? (abstract: https://jga2024.sciencesconf.org/581190)

Sémantique
Mardi 12 novembre 2024, 15 heures, Salle 3071
Pedro Amorim (Oxford) A Unified Approach to Markov Kernels and Linear Operators

In recent years, there has been much work done in probabilistic semantics. Most of them fall in one of two categories; those based on monads and those based on linear logic. At the semantic level, these two different semantics correspond to distinct basic programming abstractions. In this case, semantically, programming with monads corresponds to programming with Markov kernels, while linear logic corresponds to programming with linear operators.

In this talk I will go over recent work of mine that tries to establish a formal connection between these two families of semantics. I will start by presenting a new core calculus for programming with Markov kernels and linear operators, will show that this formalism encompasses useful models from the probabilistic semantics literature and will conclude by sketching some applications of this formalism to the new research program of synthetic probability theory.

Soutenances de thèses
Mardi 12 novembre 2024, 16 heures, Halle aux Farines, Room 580F (salles des thèses) & zoom : https://u-paris.zoom.us/j/5848945659? (Password: 248469)
Clément Ducros Multi-Party Computation Based on the Computational Hardness of Coding Theory

Since the beginning of modern cryptography, the question of secure computation (MPC) has been extensively studied. MPC allows for a set of parties to perform some joint computation while ensuring that their input remains secure up to what is implied by the output. The massive development of our daily Internet usage makes the need for secure computation methods more urgent: computations on private data is everywhere, from recommendation algorithms to electronic auctions. Modern MPC algorithms greatly benefit from correlated randomness to achieve fast online protocols. Correlated randomness has to be massively produced beforehand for the MPC protocols to work best, and this is still a challenge to do efficiently today.

In this thesis, we study pseudorandom correlation generators (PCGs). This construction transforms a small amount of correlated randomness into a large amount of correlated pseudorandomness with minimal interaction and local computation. We present different PCG constructions whose security relies on variants of the Syndrome Decoding (SD) assumption, a classical assumption in coding theory. The intuition behind these constructions is to merge the SD assumption with some MPC techniques that enable additively sharing sparse vectors. We achieve state-of-the-art results regarding secure computation protocols requiring more than two players when the computation is over a finite field of size > 2. We show how to remove this constraint at the cost of a small overhead in communication.

Next, we consider the construction of pseudorandom correlation functions (PCFs). PCFs produce correlations on-the-fly: players each hold correlated functions such that the outputs of the functions, when evaluated on the same entry, are correlated. These objects offer more flexibility than PCGs but are also harder to construct. We again rely on variants of SD to construct PCFs. We build on a previous PCF construction, showing that the associated proof of security was incorrect, and propose a correction. Additionally, we present optimizations of the construction, coming from a better analysis and precise optimization of parameters via simulations. We achieve parameters usable in practice.

Finally, this thesis revolves around the use of certain codes, particularly the SD assumption. The search for good complexity entails efforts to find the most efficient codes while ensuring that security is not compromised. We consider a framework tailored to the study of promising attacks on SD and its variants. For each construction previously mentioned, we conduct a thorough security analysis of the associated variant of SD and attempt cryptanalysis efforts to compute concrete parameters.

One world numeration seminar
Mardi 12 novembre 2024, 14 heures, Online
Florian Luca (Stellenbosch University) On a question of Douglass and Ono

It is known that the partition function $p(n)$ obeys Benford's law in any integer base $b\ge 2$. A similar result was obtained by Douglass and Ono for the plane partition function $\text{PL}(n)$ in a recent paper. In their paper, Douglass and Ono asked for an explicit version of this result. In particular, given an integer base $b\ge 2$ and string $f$ of digits in base $b$ they asked for an explicit value $N(b,f)$ such that there exists $n\le N(b,f)$ with the property that $\text{PL}(n)$ starts with the string $f$ when written in base $b$. In my talk, I will present an explicit value for $N(b,f)$ both for the partition function $p(n)$ as well as for the plane partition function $\text{PL}(n)$.

Preuves, programmes et systèmes
Jeudi 14 novembre 2024, 13 heures, Salle 3052
Manuel Serrano (Inria) Non encore annoncé.

La syntaxe rencontre la sémantique
Jeudi 14 novembre 2024, 14 heures 30, Salle 3052
Adrienne Lancelot (LIX et IRIF) Interaction Equivalence

Contextual equivalence is the de facto standard notion of program equivalence. A key theorem is that contextual equivalence is an equational theory. Making contextual equivalence more intensional, for example taking into account the time cost of the computation, seems a natural refinement. Such a change, however, does not induce an equational theory, for an apparently essential reason: cost is not invariant under reduction.

In the paradigmatic case of the untyped λ-calculus, we introduce interaction equivalence. Inspired by game semantics, we observe the number of interaction steps between terms and contexts but—crucially—ignore their own internal steps. We prove that interaction equivalence is an equational theory and we characterize it as B, the well-known theory induced by Böhm tree equality. Ours is the first observational characterization of B obtained without enriching the discriminating power of contexts with extra features such as non-determinism. To prove our results, we develop interaction-based refinements of the Böhm-out technique and of intersection types.

Automates
Vendredi 15 novembre 2024, 14 heures, Salle 3052
Luc Dartois (LACL) Reversible Transducers over Infinite Words

Deterministic two-way transducers capture the class of regular functions. The efficiency of composing two-way transducers has a direct implication in algorithmic problems related to synthesis, where transformation specifications are converted into equivalent transducers. These specifications are presented in a modular way, and composing the resultant machines simulates the full specification. In this talk, I will present how we can achieve efficient composition of two-way transducers, mainly through the use of Reversible Transducers. Reversible machines are machine that are both deterministic and codeterministic. I will show how any two-way transducers can be made reversible, while being easily composable. I will also show how these results can be extended to the setting of infinite words, which is the dedicated setting for model-checking for example.