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 Twitter/X et LinkedIn pour suivre toute notre actualité :

Twitter/X LinkedIn

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.

5.2.2024
Rejoignez l'IRIF en tant que Responsable de la gestion financière ! Au sein d'une équipe administrative encadrée par le responsable administratif et composée de 5 agents (dont 3 gestionnaires sous votre responsabilité), vous organiserez les missions relatives à la réalisation, la mise en œuvre et le suivi des opérations financières. Date limite de candidature : vendredi 23 février 2024. | Date d'embauche prévue : 1er mars 2024

31.1.2024
Quelle politique pour la recherche ? Dans une tribune du journal l'Humanité, Claire Mathieu expose l'importance de la recherche pour la France et l'urgence à redonner de l'attractivité à ce domaine, au risque de faire fuir les jeunes chercheurs.

29.1.2024
Un poste de professeur des universités et deux postes de maître de conférence ouvrent bientôt à l'IRIF. La maîtrise du français est obligatoire pour ces postes. La date limite de dépôt des candidatures est fixée au 6 mars 2024 (16h00 - heure de Paris).

david_saulpic-scaled.jpg

1.2.2024
Nous sommes très heureux d'accueillir dès aujourd'hui David Saulpic, chargé de recherche au sein de l'IRIF. Son sujet de prédilection ? Les algorithmes, et plus particulièrement les problèmes liés au clustering. Vous pouvez le rencontrer dans son bureau 4029A.

david_saulpic-scaled.jpg

15.1.2024
Congratulations to David Saulpic, who will be joining IRIF on 1 February, winner of the 2023 Gilles Kahn Dissertation Prize! He defended his thesis in 2018, entitled “Approximation Algorithms and Sketches for Clustering”.

perso-pierre-fraigniaud.jpg

9.1.2024
Congratulations to Pierre Fraigniaud, who won an Imre Simon Test-of-Time award 2024 for the paper "Collective Tree Exploration" with Leszek Gasieniec, Dariusz R. Kowalski, and Andrzej Pelc. It appeared in the proceedings of the 6th Latin American Symposium on Theoretical Informatics (LATIN 2004). It will be delivered at the 16th edition of LATIN, in Puerto Varas, Chile, March 18-22, 2024.

imdea.jpg

24.1.2024
Le 23 janvier, Loïc Peyrot, doctorant à l’IRIF, était invité comme conférencier sur le thème « Record polymorphism for set-theoretic types » à l’IMDEA Software Institute.


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

Automates
Vendredi 23 février 2024, 14 heures, Salle 3052
Sven Dziadek (Inria Paris) Acceptance Conditions for Weighted ω-Automata

Ésik and Kuich extended the theory of weighted formal languages to infinite words in 2005. There, automata are matrices over a semiring and Büchi acceptance is an operation over those matrices. We are trying to extend the theory to other acceptance conditions (Muller, generalized Büchi, etc.) and face several challenges. Mainly, the former operator allows for a disjunction of constraints but now we need conjunction.

I will introduce the theory and detail those challenges.

Joint work with Uli Fahrenberg.

Graph Transformation Theory and Applications
Vendredi 23 février 2024, 15 heures, online
Arend Rensink (University of Twente) In the Groove - Part 2

Tooling is essential for practical applications in any field. For Graph Transformation, one of the ways to quickly prototype your graph-like domain is by developing a model in GROOVE, a standalone tool that will give you isomorphism checking, state space exploration, and model checking based on a graph grammar consisting of a set of (optionally typed) rules and start graph, optionally complemented with a control program.

In this second part of the tutorials on GROOVE, the following advanced features will be covered: Nested rules, rule parameters, control (functions and recipes), and model checking. Participants are invited to install a local copy of GROOVE and to download the .zip file with examples from the tutorial, which is available on the event's GReTA page.

Zoom meeting registration link

YouTube live stream

Vérification
Lundi 26 février 2024, 11 heures, 3052 and Zoom link
Loïc Germerie Guizouarn (Université Paris-Est Créteil) Quasi-synchronous communications and verification of distributed systems

Distributed systems are typically based on asynchronous exchanges of messages. Communicating automata are a tool to reason formally on the communications of such systems, allowing to detect automatically errors, like deadlocks or loss of messages. Detecting these errors is undecidable in general for systems with two or more participants, and several restrictions of the model have been considered to restore decidability. The subject of this presentation is one of these approaches, based on systems whose executions are realisable with synchronous communications (RSC). The behaviour of these systems approximate synchronous behaviours, where messages are sent and received in an atomic action.

Formath
Lundi 26 février 2024, 14 heures, 3052
Julien Narboux (Université de Strasbourg) Formalization of geometry, and automated theorem proving using constraint solving

In this talk, we will present a quick overview of our work (with Michael Beeson, Pierre Boutry, Gabriel Braun and Charly Gries) about formalization of geometry and the GeoCoq library. We will delve into the axiomatic systems of influential mathematicians such as Euclid, Hilbert and Tarski and present formalization issues. A special focus will be placed on the formalization of continuity axioms and parallel postulates. We will highlight details and issues that can be seen only through the lens of a proof assistant and intuitionistic logic. We will present a syntactic proof of the independence of the parallel postulate. From axiomatic foundations to computer-assisted proofs, we will explore the interplay between synthetic and analytic geometry, and different kinds of automation. Finally, we will present our recent work on Larus (with Predrag Janičić): a theorem prover based on coherent logic and constraint solving which can output proofs that are both readable and machine checkable, along with illustrations generated semi-automatically.

Combinatoire énumérative et analytique
Mardi 27 février 2024, 11 heures, Salle 1007
Gilles Schaeffer From catalytic to algebraic decomposition, bijectively.

A celebrated result of Bousquet-Mélou and Jehanne states that under reasonable combinatorial hypotheses the solutions of polynomial equations with one catalytic variable are algebraic series. We give a combinatorial derivation of this result in the case of order one catalytic equations (those involving only one univariate unkown series), in the form of a recipe to derive systematically an algebraic decomposition or a bijection with a simply generated family of trees from an order one catalytic decomposition.

Join work with Enrica Duchi

Algorithmes et complexité
Mardi 27 février 2024, 11 heures, Salle 3052
Sophie Huiberts (LIMOS, Clermont-Ferrand) Open problems about the simplex method

The simplex method is a very efficient algorithm. In this talk we see a few of the state-of-the-art theories for explaining this observation. We will discuss what it takes for a mathematical model to explain an algorithm’s qualities, and whether existing theories meet this bar. Following this, we will question what the simplex method is and if the theoretician's simplex method is the same algorithm as the practitioner's simplex method.

Algorithmes et complexité
Mardi 27 février 2024, 14 heures, Salle 3052
Christian Konrad (University of Bristol) An Unconditional Lower Bound for Two-Pass Streaming Algorithms for Maximum Matching Approximation

In this talk, I will discuss a recent joint work with my PhD student Kheeran Naidu on lower bounds for the Maximum Matching problem in the semi-streaming model. In this model, an algorithm performs multiple passes over the edges of an input graph and is tasked with computing a matching that is as large as possible using space O(n polylog n), where n is the number of vertices of the input graph.

We will focus on the two-pass setting, and we show that every randomized two-pass streaming algorithm that computes a better than 8/9-approximation to Maximum Matching requires strictly more than semi-streaming space.

Prior to our work, only a conditional two-pass lower bound by Assadi [SODA'22] was known that relates the quality of their lower bound to the maximum density of Ruzsa-Szemeredi graphs (RS-graphs) with matchings of linear sizes. In the best case, i.e., if very dense RS-graphs with linear-sized matchings exist, their lower bound rules out approximation ratios above 0.98, however, with current knowledge, only approximation factors of 1 − o(1) are ruled out.

Our lower bound makes use of the information cost trade-off of the Index problem in the two-party communication setting established by Jain et al. [JACM’09]. To the best of our knowledge, our work is the first that exploits this trade-off result in the context of lower bounds for multi-pass graph streaming algorithms.

Automates
Jeudi 29 février 2024, 14 heures, Salle 3052
Ivan Varzinczak An Introduction to Defeasible Description Logics

Description Logics (DLs) are a family of logic-based knowledge representation formalisms with appealing computational properties and various applications at the confluence of artificial intelligence, databases and other areas. In particular, DLs are well-suited for representing and reasoning about ontologies; therefore, they stand as the formal foundations of the Semantic Web. The different DL formalisms that have been proposed in the literature provide us with a wide choice of constructors in the object language. Nevertheless, these are intended to represent only classical, unquestionable knowledge and, therefore, cannot express and cope with the different aspects of uncertainty and vagueness that often appear in everyday life. Examples of these comprise the various guises of exceptions, typicality (and atypicality), approximations and many others, as usually encountered in the different forms of everyday human reasoning. A similar argument can be put forward when moving to the level of entailment, that of the sanctioned conclusions from an ontology. DL systems provide a variety of (standard and non-standard) reasoning services. Still, the underlying notion of entailment remains classical. Therefore, depending on the application one has in mind, DLs inherit most of the criticisms raised in the development of the so-called non-classical logics. In this talk, I make a case for endowing DLs and their associated reasoning services with the ability to cope with defeasibility. I start by introducing the notion of defeasible class subsumption, which allows for the specification of and reasoning about defeasible inheritance. I also show how it can be given an intuitive semantics in terms of preference relations. Next, I show how to take defeasibility to the level of entailment through the notion of rational closure of a defeasible ontology. Of particular interest is the fact that our constructions do not negatively affect the decidability or complexity of reasoning with defeasible inheritance for a wide class of DLs.

Speaker's short CV: Ivan Varzinczak is an associate professor at Université Paris 8. He holds a PhD (2006) in artificial intelligence from Université Paul Sabatier, France. Ivan has co-authored over 75 peer-reviewed publications on logic-based approaches to knowledge representation and reasoning in AI. In 2019 he defended his habilitation at Université d'Artois, France. Ivan is an associate editor of Artificial Intelligence and of the Journal of Artificial Intelligence Research and chairman of the steering committee of the International Workshop on Nonmonotonic Reasoning. In 2022, he served as program chair of the 12th International Symposium on Foundations of Information and Knowledge Systems (FoIKS). He has had several visiting researcher appointments and taught courses and tutorials worldwide, including two courses at ESSLLI and two tutorials at IJCAI.

Séminaire des membres non-permanents
Jeudi 29 février 2024, 16 heures, Salle 3052
Huan Zhou Graph colouring: Extending brooks’ Theorem

In graph theory, graph colouring is a special case of graph labelling; it is an assignment of labels traditionally called ‘’colours’’ to elements of a graph subject to certain constraints. In its simplest form, it is a way of colouring the vertices of a graph such that no two adjacent vertices are of the same colour, which is called vertex colouring. The problem of colouring a graph arises in many practical areas such as sports scheduling, designing seating plans, exam timetabling, the scheduling of taxis and so on.

In this talk, I will introduce some basic conceptions and theorems of graph colouring, such as brooks’ Theorem. Moreover, I will introduce a new conception called k-truncated-degree choosability and some open problems.

Automates
Vendredi 1 mars 2024, 14 heures, Salle 3052
Benjamin Bordais From Local to Global Optimality in Concurrent Parity Games

In two-player turn-based stochastic parity games, both players have positional optimal strategies. On the other hand, in two-player concurrent parity games, optimal strategies may not exist and playing (almost-)optimally may require infinite memory. In this talk, I will present how to identify a local condition that ensures the existence of positional optimal strategies for both players; this local condition is satisfied by more than only turn-based games. I will discuss how we have proved this result — by adapting to the concurrent setting techniques used in the turn-based deterministic setting — and what we can say about this local condition.

This is a joint work with my former PhD advisors Patricia Bouyer and Stéphane Le Roux, and it is based on a paper published in CSL 2024.