Les membres de l'IRIF et les visiteurs sont priés de se conformer aux directives COVID-19 du CNRS et de l'Université de Paris.

Institut de Recherche en Informatique Fondamentale (IRIF)


L'IRIF est une unité mixte de recherche (UMR 8243) entre le CNRS et l'Université de Paris, qui héberge deux équipes-projets 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. Six de ses membres ont été lauréats de l'European Research Council (ERC), cinq 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.

Delia Kesner

Delia Kesner (IRIF) has been elected corresponding member for information sciences of the Accademia delle Scienze di Torino.

Three papers co-authored by IRIF members will be presented at POPL2021, the main conference on programming languages and programming systems. The papers' study randomized computation, including machine learning, and verification for programs over persistent memory.

Pierre-Louis Curien

Pierre-Louis Curien (IRIF) is awarded with this year's Grand prix Inria – Académie des sciences. To learn more about Pierre-Louis Curien's contributions to theoretical computer science, read the portrayal published by Inria, and the interviews published by FSMP and La Recherche.

Claire Mathieu

A paper by C. Mathieu (IRIF CNRS member) with R. Rajaraman, N. Young, and A. Yousefi will be presented at SODA2021 on dynamization policies in the competitive analysis framework for log-structured merge trees underpinning industrial NoSQL databases.

Geoffroy Couteau

A paper by G. Couteau (IRIF CNRS researcher) and D. Hartmann has been presented at the conference CRYPTO2020 and describes new, more compact constructions of non-interactive zero-knowledge proofs in elliptic curves equipped with a bilinear map.

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

Algorithmes et complexité
Mercredi 2 décembre 2020, 14 heures, Online
Claire Mathieu (IRIF) Competitive Data-Structure Dynamization

Data-structure dynamization is a general approach for making static data structures dynamic. It is used extensively in geometric settings and in the guise of so-called merge (or compaction) policies in big-data databases such as Google Bigtable and LevelDB (our focus). Previous theoretical work is based on worst-case analyses for uniform inputs – insertions of one item at a time and constant read rate. In practice, merge policies must not only handle batch insertions and varying read/write ratios, they can take advantage of such non-uniformity to reduce cost on a per-input basis. To model this, we initiate the study of data-structure dynamization through the lens of competitive analysis, via two new online set-cover problems. For each, the input is a sequence of disjoint sets of weighted items. The sets are revealed one at a time. The algorithm must respond to each with a set cover that covers all items revealed so far. It obtains the cover incrementally from the previous cover by adding one or more sets and optionally removing existing sets. For each new set the algorithm incurs build cost equal to the weight of the items in the set. In the first problem the objective is to minimize total build cost plus total query cost, where the algorithm incurs a query cost at each time t equal to the current cover size. In the second problem, the objective is to minimize the build cost while keeping the query cost from exceeding k (a given parameter) at any time. We give deterministic online algorithms for both variants, with competitive ratios of Θ(log∗n) and k, respectively. The latter ratio is optimal for the second variant.

Séminaire des doctorants
Mercredi 2 décembre 2020, 11 heures, Online
Phd Students Welcome session!

Combinatoire énumérative et analytique
Jeudi 3 décembre 2020, 10 heures, Virtuel
Marni Mishna, Laurent Viennot Séminaire Flajolet

Preuves, programmes et systèmes
Jeudi 3 décembre 2020, 10 heures 30, Online
Laure Gonnord (Université Lyon Claude Bernard) Contributions in static analyses for memory: the example of arrays

Proving the absence of bugs in a given piece of software (a problem which has been known to be intrinsically hard since Turing and Cook) is not the only challenge in software development. Indeed, the ever growing complexity of software increases the need for more trustable optimisations. Solving these two problems (reliability, optimisation) implies the development of safe (without false negative answers) and efficient (wrt memory and time) analyses, yet precise enough (with few false positive answers).

In this talk I will present two experiences in the design of static analyses dedicated to array properties and explore the intrinsic difficulties we, together with my coauthors, faced while developing them. I will also show some experimental evidence of the impact of this work on real-world compilers, as well as future perspective for this area of research.

Vendredi 4 décembre 2020, 14 heures 30, Salle 3052
Georg Zetzsche Rational subsets of Baumslag-Solitar groups

We consider the rational subset membership problem for Baumslag-Solitar groups. These groups form a prominent class in the area of algorithmic group theory, and they were recently identified as an obstacle for understanding the rational subsets of GL(2,ℚ). We show that rational subset membership for Baumslag-Solitar groups BS(1,q) with q ≥ 2 is decidable and PSPACE-complete. To this end, we introduce a word representation of the elements of BS(1,q): their pointed expansion (PE), an annotated q-ary expansion. Seeing subsets of BS(1,q) as word languages, this leads to a natural notion of PE-regular subsets of BS(1,q): these are the subsets of BS(1,q) whose sets of PE are regular languages. Our proof shows that every rational subset of BS(1,q) is PE-regular. Since the class of PE-regular subsets of BS(1,q) is well-equipped with closure properties, we obtain further applications of these results. Our results imply that (i) emptiness of Boolean combinations of rational subsets is decidable, (ii) membership to each fixed rational subset of BS(1,q) is decidable in logarithmic space, and (iii) it is decidable whether a given rational subset is recognizable. In particular, it is decidable whether a given finitely generated subgroup of BS(1,q) has finite index.

This is joint work with Michaël Cadilhac and Dmitry Chistikov.

Soutenances de thèses
Vendredi 4 décembre 2020, 14 heures, Online
Isaac Konan (IRIF) Rogers-Ramanujan type identities: bijective proofs and Lie-theoretic approach

The topic of this thesis belongs to the theory of integer partitions, at the intersection of combinatorics and number theory. In particular, we study Rogers-Ramanujan type identities in the framework of the method of weighted words. This method revisited allows us to introduce new combinatorial objects beyond the classical notion of integer partitions: the generalized colored partitions. Using these combinatorial objects, we establish new Rogers-Ramanujan identities via two different approaches. The first approach consists of a combinatorial proof, essentially bijective, of the studied identities. This approach allowed us to establish some identities generalizing many important identities of the theory of integer partitions: Schur’s identity and Göllnitz’ identity, Glaisher’s identity generalizing Euler’s identity, the identities of Siladi´c, of Primc and of Capparelli coming from the representation theory of affine Lie algebras. The second approach uses the theory of perfect crystals, coming from the representation theory of affine Lie algebras. We view the characters of standard representations as some identities on the generalized colored partitions. In particular, this approach allows us to establish simple formulas for the characters of all the level one standard representations of type A_{n-1}^{(1)},A_{2n}^{(2)},D_{n+1}^{(2)},A_{2n-1}^{(2)},B_{n}^{(1)},D_{n}^{(1)}.

Graph Transformation Theory and Applications
Vendredi 4 décembre 2020, 15 heures, (online)
Daniel Merkle & Jakob Lykke Andersen (Department of Mathematics and Computer Science, University of Southern Denmark, Odense, Denmark) Chemical Graph Transformation and Applications

Any computational method in chemistry must choose some level of precision in the modeling. One choice is made in the methods of quantum chemistry based on quantum field theory. While highly accurate, the methods are computationally very demanding, which restricts their practical use to single reactions of molecules of moderate size even when run on supercomputers. At the same time, most existing computational methods for systems chemistry and biology are formulated at the other abstraction extreme, in which the structure of molecules is represented either not at all or in a very rudimentary fashion that does not permit the tracking of individual atoms across a series of reactions.

In this talk, we present our on-going work on creating a practical modelling framework for chemistry based on Double Pushout graph transformation, and how it can be applied to analyse chemical systems. We will address important technical design decisions as well as the importance of methods inspired from Algorithm Engineering in order to reach the required efficiency of our implementation. We will present chemically relevant features that our framework provides (e.g. automatic atom tracing) as well as a set of chemical systems we investigated are currently investigating. If time allows we will discuss variations of graph transformation rule compositions and their chemical validity.

Zoom registration link:


Link to YouTube live stream:


Lundi 7 décembre 2020, 11 heures, BBB link
Marie Fortin (University of Liverpool) Logics and automata over infinite message sequence charts

Communicating finite-state machines (CFMs) are a standard model of concurrent message-passing systems. They consist of a fixed number of finite-state processes communicating through unbounded point-to-point FIFO channels, and they define languages of partial orders called message sequence charts (MSCs), representing possible executions of the system. In this talk, I will review past and recent characterizations of the expressive power of CFMs, in the spirit of Büchi-Elgot-Trakhtenbrot theorem for finite automata. Our main result is that, both for finite and infinite executions, CFMs have the same expressive power as existential monadic second-order logic (EMSO). As a corollary, we obtain a new proof of a known characterization in the restricted case where the channels are assumed to be of bounded size, namely, that CFMs are equivalent to full MSO logic over finite existentially-bounded MSCs. We also extend that result from finite to infinite executions. For the main result, where channels are assumed to be unbounded, the proof relies on another logic of independent interest: a star-free variant of propositional dynamic logic based on operations similar to LTL “since” and “until” modalities. This logic is equivalent to first-order logic, and its formulas can be translated into equivalent CFMs of exponential size (on the other hand, the translation from first-order logic is non-elementary). This is joint work with Benedikt Bollig and Paul Gastin.

One world numeration seminar
Mardi 8 décembre 2020, 14 heures 30, Online
Tanja Isabelle Schindler (Scuola Normale Superiore di Pisa) Limit theorems on counting large continued fraction digits

We establish a central limit theorem for counting large continued fraction digits (a_n), that is, we count occurrences {a_n>b_n}, where (b_n) is a sequence of positive integers. Our result improves a similar result by Philipp, which additionally assumes that bn tends to infinity. Moreover, we also show this kind of central limit theorem for counting the number of occurrences entries such that the continued fraction entry lies between d_n and d_n (1+1/c_n) for given sequences (c_n) and (d_n). For such intervals we also give a refinement of the famous Borel–Bernstein theorem regarding the event that the nth continued fraction digit lying infinitely often in this interval. As a side result, we explicitly determine the first φ-mixing coefficient for the Gauss system - a result we actually need to improve Philipp's theorem. This is joint work with Marc Kesseböhmer.

Combinatoire énumérative et analytique
Mercredi 9 décembre 2020, 10 heures 30, Virtuel
Helen Jenne (LMPT et Université de Tours) Non encore annoncé.