Bienvenue L'IRIF est une unité mixte de recherche (UMR 8243) entre le CNRS et l'Université Paris Cité, qui 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. Notion du jour Réseaux Sociaux Suivez nous sur Twitter/X et LinkedIn pour suivre toute notre actualité : Actualités 7.12.2023 Nous sommes très fiers d'annoncer que Claire Mathieu, directrice de recherche (CNRS) fait partie du conseil présidentiel de la science annoncé ce jeudi 7 décembre 2023. “Ce groupe de douze scientifiques de haut niveau doit fournir des conseils à l'exécutif pour orienter sa politique de recherche et d'innovation […]”. 24.11.2023 Sylvain Perifel will defend his habilitation to direct research [HDR] on Monday 4 December 2022 at 2pm in the Pierre-Gilles de Gennes Amphitheatre of the Condorcet building. His subject is L'aléatoire par le prisme des polynômes et de la compression. 30.11.2023 IRIF has the great pleasure to welcome a new researcher (INRIA ISFP): Guillaume Baudart, an expert in on probabilistic and reactive programming languages (language design, semantics, static analysis, compilation, inference). 16.11.2023 La prochaine édition de Mathématiques en mouvement, conférence proposée par la FSMP, aura pour thème Des preuves et des programmes. Organisée sous la houlette de Hugo Herbelin, elle aura lieu le samedi 2 décembre 2023 de 14h à 18h. 23.11.2023 IRIF has the great pleasure to welcome a new researcher (INRIA): Gabriel Scherer, an expert in programming languages, with theoretical aspects of type systems, programming language implementation, general programming language concepts, and even some syntactic aspects. 21.11.2023 Du mardi 28 novembre au jeudi 30 novembre, nous recevrons à l'IRIF le comité d'évaluation de l'HCERES dans le cadre de l'évaluation de notre laboratoire. Programme 10.10.2023 We are very proud to announce that five papers by six IRIF researchers have been selected for the CSL conference! Congratulations to Quentin Aristote, Guillaume Geoffroy, Roman Kniazev, Jérémy Ledent, François Laroussinie and Vincent Moreau. 14.11.2023 We are very proud to announce that two papers by two IRIF researchers have been selected for the SODA conference! Congratulations to François Sellier and Robin Vacus. edit toutes les anciennes actualités (Ces actualités sont présentées selon un classement mêlant priorité et aléatoire.) Agenda Combinatoire énumérative et analytique Jeudi 7 décembre 2023, 10 heures, IHP Séminaire Flajolet Et Conférence Ihp: Computer Algebra For Functional Equations In Combinatorics And Physics Du 4 Au 8 Décembre. Conférence à l'IHP incluant une journée spéciale “Séminaire Flajolet” le jeudi 7. Inscription obligatoire sur le site de la conférence: https://indico.math.cnrs.fr/event/8115/registrations/ Voir aussi: https://semflajolet.math.cnrs.fr/ Preuves, programmes et systèmes Jeudi 7 décembre 2023, 10 heures 30, Salle 3052 & online (Zoom link) Meven Lennon-Bertrand (Université de Cambridge) Towards a certified proof assistant kernel – What it takes and what we have Proof assistant kernels are a natural target for program certification: they are small, critical, and well-specified. Still, despite the maturity of the field of software certification, we are yet to see a certified Agda, Coq or Lean. In this talk, I will try and explain why this is not such an easy task, and present two complementary projects going in that direction. The first, MetaCoq, is a large scale project, broadly aiming at giving tools to manipulate Coq terms and derivations inside of Coq, in particular developing an important body of formalized proofs around Coq's typing. The second is a more recent endeavour, aimed at tackling the mother of all properties: normalisation. Séminaire des membres non-permanents Jeudi 7 décembre 2023, 16 heures, Salle 3052 Esaie Bauer Proof theory in Multiplicative-Additive Linear Logic In this presentation, I will provide an introduction to proof theory within the context of non-wellfounded proof systems. A non-wellfounded proof is generated by finitely branching logical rules, but potentially resulting in an infinitely deep proof tree. After defining the system, I will present a proof of cut-elimination for the $\mu$-MALL system, drawing from the work of Baelde et al. in 2016. Furthermore, I will discuss how we aim to extend this result with Alexis Saurin. La syntaxe rencontre la sémantique Jeudi 7 décembre 2023, 14 heures, Salle 3052 Pablo Barenbaum (Universidad Buenos Aires) Sharing in linear logic and call-by-need Automates Vendredi 8 décembre 2023, 14 heures, Salle 3052 Anantha Padmanabha Consistent Query Answering under Primary Keys Primary key constraints in databases state there can be at most one tuple for every primary key in a given relation. However, these days it is common to have situations where this property cannot be maintained. Databases that violate constraints are called « inconsistent databases ». In particular, if a database violates primary key constraint, it will contain more than one tuple for the same primary key. In this setting, the notion of a repair is defined by picking exactly one tuple for each primary key (maximal consistent subset of the database). A Boolean conjunctive query q is certain for an inconsistent database D if q evaluates to true over all repairs of D. In this context, there is a dichotomy conjecture that states that for a fixed boolean conjunctive query q, testing whether q is certain for an input database D is either polynomial time or coNP-complete. The conjecture is open in general and has been open for more than two decades. In this talk we will introduce two new algorithms that we have devised, one based on fix-point computation and the other based on bipartite matching. We will also see how these algorithms can be used to prove the dichotomy for the cases that were previously open. These results were obtained in collaboration with Diego Figueira, Luc Segoufin and Cristina Sirangelo and combine the results that were presented at ICDT 2023 and what will be presented at PODS 2024. Algorithmique distribuée et graphes Vendredi 8 décembre 2023, 15 heures, 1007 Pierre Aboulker (ENS-Paris) Clique number of tournaments the dichromatic number of a digraph is the minimum integer k such that the set of vertices of D can be partitioned into k acyclic subdigraphs. It is easy to see that the chromatic number of a graph G is the same as the dichromatic of the digraph obtained from G by replacing each edge by a digon (two anti-parallel arcs). Based on this simple observation, many theorems concerned with chromatic number of undirected graphs have been generalised to digraphs via the dichromatic number. However, no concept of clique number for digraphs was available. The purpose of this presentation is to explore such a concept and its relationship with the dichromatic number, mirroring the relationship between the clique number and chromatic number in undirected graphs. We will focus on studying the notion of chi-boundedness in particular. This is a joint work with Guillaume Aubian, Pierre Charbit and Raul Lopes. La théorie des types et la théorie de l'homotopie Vendredi 8 décembre 2023, 15 heures 30, Salle 3052 Moana Jubert Prérequis homotopiques de la théorie des types homotopiques Vérification Lundi 11 décembre 2023, 11 heures, 3052 and Zoom link Sarah Winter (IRIF) Non encore annoncé. Combinatoire énumérative et analytique Mardi 12 décembre 2023, 11 heures, Salle 1007 Philippe Nadeau Non encore annoncé. Algorithmes et complexité Mardi 12 décembre 2023, 11 heures, Salle 3052 Deeksha Adil (ETH Zurich) Dynamically Computing Approximate Eigenvectors Maintaining spectral information quickly with changing data matrix is essential in several applications. In this talk I would give an overview of what is known in this area and present a simple yet novel algorithm and analysis of maintaining an approximate maximum eigenvalue and eigenvector of a positive semi-definite matrix quickly, that undergoes decremental updates. Our algorithms also hint towards a separation between oblivious and adaptive adversaries in the dynamic setting, which has not yet been resolved. This is based on a very recent work with Thatchaphol Sararunak.