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

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.

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

perso-claire-mathieu.jpg

2.1.2024
Following the adoption of the immigration law by the government, Claire Mathieu resigned from the Presidential Science Council, which was set up on 7 December 2023.

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).

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.

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.

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.


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

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.

La théorie des types et la théorie de l'homotopie
Vendredi 1 mars 2024, 15 heures 30, Salle 3052
Sylvain Douteau Homotopy theory of simplicial sets

Vérification
Lundi 4 mars 2024, 11 heures, 3052 and Zoom link
Adrian Francalanza (University of Malta) Non encore annoncé.

Formath
Lundi 4 mars 2024, 14 heures, 3052
Guillaume Baudart Schedule Agnostic Semantics for Reactive Probabilistic Programming

Synchronous languages are now a standard industry tool for critical embedded systems. Designers write high-level specifications by composing streams of values using block diagrams. These languages have been extended with Bayesian reasoning to program state-space models which compute a stream of distributions given a stream of observations. Yet, the semantics of probabilistic models is only defined for scheduled equations – a significant limitation compared to dataflow synchronous languages and block diagrams which do not require any ordering.

In talk I will present two schedule agnostic semantics for a probabilistic synchronous language. The key idea is to interpret probabilistic expressions as a stream of un-normalized density functions which maps random variable values to a result and positive score. The co-iterative semantics extends the original semantics to interpret mutually recursive equations using a fixpoint operator. The relational semantics directly manipulates streams and is thus a better fit to reason about program equivalence. We use the relational semantics to prove the correctness of a program transformation required to run an optimized inference algorithm for state-space models with constant parameters.

This is joint work with Louis Mandel and Christine Tasson.

Combinatoire énumérative et analytique
Mardi 5 mars 2024, 11 heures, Salle 3058
Eleanor Archer Non encore annoncé.

Preuves, programmes et systèmes
Jeudi 7 mars 2024, 11 heures, Salle 3052
Jérôme Feret (École normale supérieure) Non encore annoncé.

Séminaire des membres non-permanents
Jeudi 7 mars 2024, 16 heures, Salle 3052
Christoph Egger Proving Negative Results: Oracle Separations

We're all used to and familiar with proving interesting results and of course sometimes we can also prove that theorems are wrong. But is there something substantial one can say about the absence of proofs? The more philosophically inclined can go back to Gödel's famous work and convince themselves that there will always be true statements that are not provable in any particular system.

As such a statement will necessarily depend on a concrete theory of proof we are going to look into a specific technique commonly used in complexity theory called oracle separations (Impagliazzo, Rudich, STOC 1989) and how we can use an elementary counting argument to create a contradiction to proofs (Gennaro, Trevisan, FOCS 2000).

Given the topic at hand we are going to struggle with too many negations. Also it comes natural to re-introduce reduction proofs but it clearly helps to have seen those already (say in undergrad np completeness). There's virtually no cryptography in it and I assume we can keep it broadly accessible to all lab members even though it is a somewhat technical topic!

Catégories supérieures, polygraphes et homotopie
Vendredi 8 mars 2024, 14 heures, Salle 3058
Emile Oléon (Ecole polytechnique) Delooping cyclic groups with lens spaces in homotopy type theory

In the setting of homotopy type theory, each type can be interpreted as a space. Moreover, given an element of a type, i.e. a point in the corresponding space, one can define another type which encodes the space of loops based at this point. In particular, when the type we started with is a groupoid, this loop space is always a group. Conversely, to every group we can associate a type (more precisely, a pointed connected groupoid) whose loop space is this group: this operation is called delooping. The generic procedures for constructing such deloopings of groups (based on torsors, or on descriptions of Eilenberg-MacLane spaces as higher inductive types) are unfortunately equipped with elimination principles which do not directly allow eliminating to arbitrary types, and are thus difficult to work with in practice. Here, we construct deloopings of the cyclic groups Z_m which are cellular, and thus do not suffer from this shortcoming. In order to do so, we provide type-theoretic implementations of lens spaces, which constitute an important family of spaces in algebraic topology. In some sense, this work generalizes the construction of the real projective space by Buchholz and Rijke in their LICS'17 paper, which handles the case m=2, although the general setting requires more involved tools. Finally, we use this construction to also provide cellular descriptions of dihedral groups, and explain how we can hope to use those to compute the cohomology and higher actions of such groups.