Institut de Recherche en Informatique Fondamentale (IRIF)

CNRS

Université Paris Cité

IRIF is a research laboratory of CNRS and Université Paris Cité, also hosting one Inria project-team.

The research conducted at IRIF is based on the study and understanding of the foundations of all computer science, in order to provide innovative solutions to the current and future challenges of digital sciences.

IRIF hosts about 200 people. Seven of its members have been distinguished by the European Research Council (ERC), six are members of the Institut Universitaire de France IUF), two are members of the Academia Europæa, and one is member of Académie des sciences.

Follow us on Twitter/X and LinkedIn for our latest news:

Twitter/X LinkedIn

30.1.2024
How to design algorithms to analyze protocols in electronic voting ? How to define mathematically vote secrecy ? What is at stake ? Read the interview Véronique Cortier granted us before her distinguished talk on 7 February, 2024.

31.1.2024
What kind of research policy? In an article for the french newspaper l'Humanité, Claire Mathieu explains the importance of research for France and the urgent need to make the field more attractive again, at the risk of driving away young researchers.

5.2.2024
Join IRIF as Financial Management Manager! As part of an administrative team supervised by the Administrative Manager and consisting of 5 staff (including 3 managers under your responsibility), you will organise tasks relating to the preparation, implementation and monitoring of financial operations. Application deadline: Friday 23 February 2024. | Planned start date: 1 March 2024

david_saulpic-scaled.jpg

1.2.2024
We are delighted to welcome David Saulpic, Research Fellow at the IRIF. His favourite subject? Algorithms, and more specifically clustering problems. You can meet him in his office 4029A.

29.1.2024
One full professor (professeur des universités) and two associate professor (maître de conference) positions will open at IRIF. Fluency in French is mandatory for these positions. The application deadline is March the 6th 2024 (16h00 - Paris time)

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.

perso-frederic-magniez.jpg

22.12.2023
Frédéric Magniez,CNRS research director at IRIF and former professor at the Collège de France, was the technical president of the « The Blaise Pascal [re]Generative Quantum Challenge » jury. It was organised by Pasqal, in collaboration with Blaise Pascal Advisors, Michelin, GENCI, and Capgemini. In this interview, he explains the objectives of the challenge and the importance of fundamental research in all the solutions found:

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.

(These news are displayed using a randomized-priority ranking.)

Proofs, programs and systems
Thursday February 22, 2024, 11AM, Salle 3052 & online (Zoom link)
Adrienne Lancelot (IRIF, Université Paris Cité & INRIA, LIX, Ecole Polytechnique) Light Genericity

To better understand Barendregt's genericity for the untyped call-by-value lambda-calculus, we start by first revisiting it in call-by-name, adopting a lighter statement and establishing a connection with contextual equivalence. Then, we use it to give a new, lighter proof of maximality of head contextual equivalence, i.e. that H* is a maximal consistent equational theory. We move on to call-by-value, where we adapt these results and also introduce a new notion dual to light genericity, that we dub co-genericity. We present light (co-)genericity as robust properties rather than just lemmas and provide different proofs based on applicative bisimilarity, semantic models and direct rewriting techniques.

Automata
Friday February 23, 2024, 2PM, 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
Friday February 23, 2024, 3PM, 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

Verification
Monday February 26, 2024, 11AM, 3052 and Zoom link
Loïc Germerie Guizouarn (Université Paris-Est Créteil) To be announced.

Formath
Monday February 26, 2024, 2PM, 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.

Enumerative and analytic combinatorics
Tuesday February 27, 2024, 11AM, 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

Algorithms and complexity
Tuesday February 27, 2024, 11AM, 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.

Algorithms and complexity
Tuesday February 27, 2024, 2PM, 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.

Automata
Thursday February 29, 2024, 2PM, 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.

Non-permanent members' seminar
Thursday February 29, 2024, 4PM, Salle 3052
Huan Zhou To be announced.