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

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.

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.

affichefds2024.jpg

4.10.2024
La Fête de la Science édition 2024 est lancée ! L'IRIF et l'Université Paris Cité accueilleront du 4 au 14 octobre, 13 classes de primaire et collège, qui viendront découvrir l'informatique à travers des activités débranchées et de la programmation. Nous proposons également un programme quantique créé avec le laboratoire Matériaux et Phénomènes Quantiques (MPQ) à des classes de lycée.

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.

perso-delia-kesner.jpg

26.8.2024
Delia Kesner est oratrice invitée à la conférence internationale Lambda World qui aura lieu à Cadiz (Espagne) du 2 au 4 octobre 2024.

book_basics_of_programming_algorithms.jpeg

11.9.2024
Roberto Mantaci et Jean-Baptiste Yunès ont publié un livre intitulé « Basics of Programming and Algorithms, Principles and Applications ». Il fournit un contenu de base pour l'enseignement de la programmation et des algorithmes, couvrant l'analyse des performances des algorithmes et les connaissances essentielles en programmation Python.

perso_robinvacus.jpg

5.9.2024
Le comité du prix de thèse de doctorat 2024 Principles of Distributed Computing a décidé de partager le prix entre deux lauréats, dont Robin Vacus pour sa thèse « Algorithmic Perspectives to Collective Natural Phenomena » (Perspectives algorithmiques sur les phénomènes naturels collectifs). Il a effectué son doctorat sous la direction d'Amos Korman et de Pierre Fraigniaud, à l'Université Paris Cité. Sa thèse applique une approche de systèmes distribués à des problèmes et des modèles inspirés de la biologie et de la sociologie.

Happy International Woman Day.Feminism concept.Bright Beautiful Different
Dancing Girls Holding Hands.Party,Eight of March Celebration. Free Confident...

19.9.2024
Cette année, l'IRIF s'est fixé un objectif clair : atteindre la parité parmi les stagiaires de 3e. Un véritable défi, car dans les sciences informatiques, la proportion de femmes est encore nettement plus faible. C'est pourquoi nous comptons sur nos réseaux pour attirer davantage de candidatures féminines que les années précédentes ! Une semaine dans notre laboratoire de recherche permettra aux stagiaires de découvrir l'univers de la recherche et de mieux comprendre ce qu'est l'informatique.


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

Catégories supérieures, polygraphes et homotopie
Vendredi 18 octobre 2024, 14 heures, Salle 1013
Anibal Medina Mardones (UWO) Framed polytopes and higher structures

A framed polytope is the convex closure of a finite set of points in Euclidean space together with an ordered linear basis. An n-category is a category that is enriched in the category of (n-1)-categories. Although these concepts may initially appear to be distant peaks in the mathematical landscape, there exists a trail connecting them, blazed in the 90's by Kapranov and Voevodsky. We will traverse this path, widening and improving it as we address some of their conjectures along the way. If time permits, using a special embedding of the combinatorial simplex, we will connect this trail to the one ascending Mount Steenrod. This connection will enable us to express the combinatorics of cup-i products in convex geometric terms, dual to those introduced earlier in the talk to define the nerve of higher categories.

Automates
Vendredi 18 octobre 2024, 14 heures, Salle 3071
Fabian Reiter (LIGM) Locality via Alternation?

In this talk, I will show how logic and automata theory can help research in distributed computing.

I will start with an attempt to use logic to extend standard complexity theory to the distributed setting. It turns out that several classical concepts generalize well, including the polynomial hierarchy (and hence the complexity classes P and NP), the Cook-Levin theorem (which identifies Boolean satisfiability as a complete problem for NP), and Fagin's theorem (which characterizes NP as the problems expressible in existential second-order logic). But perhaps more surprisingly, separating complexity classes becomes easier in the general case: when extended to multiple computers, the polynomial hierarchy is provably infinite, while it remains notoriously open whether the same holds in the case of a single computer.

In the second part of the talk, I will use the previous results to address a central question in distributed computing: which problems are purely local, which problems are inherently global, and which problems lie between these extremes? The idea will be to measure locality using quantifier alternation, the key concept underlying the polynomial hierarchy.

The talk is based on my paper “A LOCAL View of the Polynomial Hierarchy”. - Proceedings version: https://doi.org/10.1145/3662158.3662774 - Full version: https://arxiv.org/abs/2305.09538

Algorithmes et complexité
Mardi 22 octobre 2024, 11 heures, Salle 3052
Adam Wesołowski (Royal Holloway) Advances in quantum algorithms for the shortest path problem

In this talk, we will delve into quantum complexity of some graph problems: Single Pair Shortest Pathfinding (SPSP), Diameter, Radius, Eccentricity. We will shortly review the electrical network framework for graphs and proceed to discuss recent advances in quantum algorithms and lower bounds for these problems and present a number of open problems. We give an algorithm in the adjacency array model that under special conditions solves the SPSP problem in $\tilde{O}(l\sqrt{m})$ steps, and with parallelization in $\tilde{O}(\sqrt{lm})$ steps, matching the upper bound on path detection up to polylog factors, where $l$ is the length of the shortest path between the considered vertices.

Combinatoire énumérative et analytique
Jeudi 24 octobre 2024, 14 heures, Salle 3071
Mark Skandera [jour et heure inhabituels!] Une généralisation de la formule des défauts de Deodhar pour la multiplication des éléments de base de Kazhdan-Lusztig

Soit H l'algèbre de Hecke d'un groupe de Coxeter (W,S). En étudiant la base Kazhdan-Lusztig de H, Deodhar a considéré les produits C_{w^{(1)} *…* C_{w^{(k)}, où (w^{(1)},… ,w^{(k)}) est une séquence de générateurs dans S. Il a défini et a compté certains “défauts” de telles séquences pour exprimer les produits correspondants dans la base naturelle de H. Nous étendons sa définition à des séquences d'éléments plus généraux de W et exprimons ainsi des produits plus généraux dans la base naturelle de H, dans la cas où W est de type A ou BC. Ce travail a été réalisé en collaboration avec Gavin Hobbs, Tommy Parisi, et Jiayuan Wang.

Preuves, programmes et systèmes
Jeudi 24 octobre 2024, 10 heures 30, Salle 3052 & online (Zoom link)
Jean-Jacques Lévy Non encore annoncé.

Séminaire des membres non-permanents
Jeudi 24 octobre 2024, 16 heures, Room 3052
Avinandan Das (PhD Student) Fooling around with Graphs : Forcing Alice and Bob to make mistakes to prove communication lower bounds.

We are in the 2-party communication setup which is as follows. There are two players Alice and Bob who are given as inputs, graphs G_1 and G_2 respectively. They communicate with each other to compute some function f on the graph G_1 \cup G_2. How many bits of communication are required between them in order for them to compute the function f ? In this technique, we will first set up the communication model, consider graph problems like maximum matching, degeneracy and coloring in this model and then delve into the technique of fooling sets in order to arrive to communication bandwidth lower bounds for these problems in the two party set-up. Fooling set is a mechanism to design inputs for Alice and Bob such that if too few bits are communicated between them, then both of them are ``fooled'' into making mistakes. If time permits, we will also peek into the mechanism of proving lower bounds for problems in streaming model using communication lower bounds.

Automates
Vendredi 25 octobre 2024, 14 heures, Salle 3052
Isa Vialard Measuring well quasi-orders

Well quasi orderings (WQOs) are at the heart of the theory of Well-Structured Systems (WSTS), a class of computational models that brought numerous important advances for the automatic verification of infinite-state systems. Recent developments in this field links the complexity of WQO-based algorithms to ordinal measures of WQOs : the maximal order type, ordinal height and ordinal width.

One main challenge is to compute the ordinal invariants of complex well quasi-orders built from simpler well quasi-orders through classical operation, such as the Cartesian product, and high-order constructions, like the finite words embedding. In my thesis, I computed compositionally the maximal order type of the direct product, the width of the multiset embedding, and the height and width of the multiset ordering. Furthermore, I compute the width of the Cartesian product in restricted cases and studied the ordinal measures of the finite powerset.In the process, I developed several tools and techniques, notably a game-theoretical approach to computing width using the notion of quasi-incomparable families of subsets. To tackle the width of the multiset ordering, I introduced and studied a fourth ordinal invariant, the friendly order type.

One world numeration seminar
Mardi 29 octobre 2024, 14 heures, Online
Victor Shirandami (University of Manchester) Probabilistic Effectivity in the Subspace Theorem and the Distribution of Algebraic Projective Points

The celebrated Roth’s theorem in Diophantine Approximation determines the degree to which an algebraic number may be approximated by rationals. A corollary of this theorem yields a transcendence criterion for real numbers based off of their decimal expansion. This theorem, and its broad generalisation due to Schmidt, famously suffers from ineffectivity. This motivates one to address this issue in the probabilistic context, whereby one makes progress in the direction of effectivity in an appropriately defined probabilistic regime. From this analysis is derived an analogue of Khintchine's theorem for algebraic numbers, answering a question of Beresnevich, Bernick, and Dodson on a density version of Waldschmidt’s conjecture.

Programmation
Lundi 4 novembre 2024, 10 heures, 3071
Thierry Martinez (INRIA) Coq Deep Pattern-Matching using Small Inversion

I will present joint work with Pierre Boutillier, Hugo Herbelin, and Meven Lennon-Bertrand. We are implementing a new algorithm, described in Pierre's PhD thesis and further developed during Meven's internship, for pattern-matching elaboration in Coq. This algorithm starts from a richer form of pattern-matching than what is currently available by default in Coq, handling deep and multiple pattern-matching with dependent types, as proposed by Thierry Coquand in the 1990s, while targeting the same elementary form of pattern-matching present in the Coq kernel.

Most of the design challenges for this algorithm come from handling the equalities that appear at each level of deconstruction of dependent inductive values. I will compare three approaches: one proposed by Healfdene Goguen, Conor McBride, and James McKinna, which relies on the equivalence axiom between homogeneous and heterogeneous equalities (equivalent to the Uniqueness of Identity Proofs); a refinement proposed by Jesper Cockx, which avoids the need for axioms; and the encoding by small inversion, which moves the proofs of deconstruction of the dependencies from the term level to the type level. While these algorithms give an encoding of dependent pattern-matching into the Coq kernel, this discussion leads us to think about what could be a better primitive form of pattern-matching.

Combinatoire énumérative et analytique
Mardi 5 novembre 2024, 14 heures, Salle 3071
Hugo Manet [heure inhabituelle!] tba