L'IRIF est une unité mixte de recherche (UMR 8243) entre le CNRS et l'Université Paris-Diderot, 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), trois sont membres de l'Institut Universitaire de France (IUF) et deux sont membres de l'Academia Europæa.

(Ordonnées par priorité et aléatoire)

Amaury Pouly

Amaury Pouly (IRIF) with François Fages, Guillaume Le Guludec and Olivier Bournez were awarded the prize "La Recherche": they have shown that chemical reactions, as the ones taking place in cells, can simulate Turing machines. Chemical reactions are universal computers.

Yoav Rodeh (left) and Amos Korman (right)

In collaboration with Yoav Rodeh (Weizmann Institute of Science), Pierre Fraigniaud and Amos Korman from IRIF published a paper in the Journal of the ACM entitled “Parallel Bayesian Search with no Coordination”.

Fabian Reiter

Fabian Reiter (former student at IRIF) wrote a short popularisation article in the Blog Binaire of the newspaper Le Monde. This article explains (in French) some aspects of his PhD thesis, recently awarded the Honorable Mention of the Gilles Kahn prize.

Pierre Fraigniaud from IRIF organizes the Workshop Complexity and Algorithms (CoA), in the framework of GdR IM, Roscoff, France, April 1-5, 2019. The objective of this workshop is to gather the French community on design and analysis of algorithms, of all forms. Deadlines: submission by 01/02/2019, registration by 02/03/2019.

Jeremy Siek

IRIF has the great pleasure to welcome Jeremy Siek, professor at Indiana University Bloomingtom, who is visiting IRIF for five months. Jeremy is the creator of gradual typing and a world-renowed expert in typed programming languages. Meet him in office 4034a.
gradual typing

Gradual typing is a technique that allows the programmer to control which parts of a program check their type correctness (i.e., that apples are added to apples) before execution and which parts check it during their execution instead. It is often used to gradually add the before-execution check to dynamic languages, like JavaScript, which perform the check only at run-time, since it is generally better to find errors before the execution of a program rather than during its execution.
Amaury Pouly

IRIF has the great pleasure to welcome a new researcher (CNRS), Amaury Pouly, an expert in continuous models of computations, and the analysis and verification of continuous/hybrid dynamical systems.


Amélie Gheerbrand and Cristina Sirangelo from IRIF co-organize with L. Libkin, L. Segoufin, and P. Senellart, the 2019 Spring School on Theoretical Computer Science (EPIT) on Databases, Logic and Automata, to happen the 7-12 April 2019 in Marseille. Preregistration before 13 January 2019.

Uri Zwick

IRIF has the great pleasure to welcome Uri Zwick, professor at the Blavantik School of Computer Sience (University of Tel-Aviv), who is visiting for four months. His stay is financed by an FSMP chair. Uri is an expert in algorithms, data structures and games. Meet him in office 4048.

Lundi 25 février 2019, 11 heures, Salle 1007
Pierre Courtieu (CNAM) A proof framework for mobile robots protocols

Distributed algorithms are known to be very difficult to design and certify. If these algorithms need to be fault or byzantine resilient the difficulty is even greater. Examples of flawed algorithms and proofs are numerous. It is therefore a natural domain for mechanized proofs (i.e. with the help of a proof assistant): the additional work of mechanizing the proofs should be worth the effort.

We present a framework, named Pactole, for designing distributed protocols for mobile robots, stating properties about these protocols and proving these properties. We can also prove *impossibility statement* i.e. that there exists no protocol achieving some property.

Our technique cannot be compared to but can be seen as complementary to model checking in the sense that our proofs are not automated but allow for instance to conclude that a protocol is correct *for any* starting configuration, number of robots, that is not proven impossible.

Preuves, programmes et systèmes
Mardi 26 février 2019, 10 heures 30, Salle 3052
Eric Finster (Inria - Nantes) Higher Universal Algebra in Dependent Type Theory

The naive translation of set-theoretic definitions of algebraic structures (such as monoids, categories and groups) into Martin-Lof type theory is often incomplete: without additional hypotheses such as truncation or a decidable equality, these translations fail to specify the behavior of the structure with respect to higher equalities. On the other hand, a complete description of such structures is quite difficult, as it typically requires the specification of an infinite number of equations. I will present recent progress on this problem by giving a definition of a “coherent polynomial monad” internal to type theory.

Algorithmes et complexité
Mardi 26 février 2019, 11 heures, Salle 1007
Uri Zwick (Tel Aviv University) Faster k-SAT algorithms using biased-PPSZ

The PPSZ algorithm, due to Paturi, Pudlak, Saks and Zane, is currently the fastest known algorithm for the k-SAT problem, for every k>3. For 3-SAT, a tiny improvement over PPSZ was obtained by Hertli. We introduce a biased version of the PPSZ algorithm using which we obtain an improvement over PPSZ for every k>=3. For k=3 we also improve on Herli's result and get a much more noticeable improvement over PPSZ, though still relatively small. In particular, for Unique 3-SAT, we improve the current bound from 1.308^n to 1.307^n.

Joint work with Thomas Dueholm Hansen, Haim Kaplan and Or Zamir

Mardi 26 février 2019, 10 heures 30, Salle 3052
Eric Finster (INRIA) L'algèbre universelle supérieur dans la théorie des types dependants

La traduction naïve des structures ensemblistes dans la théorie des types de Martin-Lof est souvent incomplète: sans hypothèses auxiliaires, comme la decidabilité de l'égalité ou troncation, ces traductions ne spécifient pas le comportement de la structure par rapport aux égalités supérieures. Par contre, une description complète n'est pas facile puisque celle-ci exige un nombre infini d'équations. Je présenterai des progrès récent sur ce problème en donnant une définition d'une “monade polynomiale” interne à la théorie des types.

Séminaire des doctorants
Mercredi 27 février 2019, 11 heures, Salle 3052
Pierre Ohlmann (IRIF) Non encore annoncé.

Combinatoire énumérative et analytique
Jeudi 28 février 2019, 11 heures 45, Salle 1007
Sylvie Hamel (Université de Montréal) Médiane de permutations: réduction d’espace et lien avec le 3-Hitting Set Problem

Le problème de la médiane d’un ensemble de permutations est un problème d’optimisation combinatoire qui consiste à trouver une permutation, appelée médiane, qui minimise la somme des distances de celle-ci aux permutations de l’ensemble. Dans cet exposé, c’est la distance de Kendall-tau qui sera utilisée. Cette distance compte le nombre de paires d’éléments dont l’ordre relatif est en désaccord entre deux permutations. Sous cette distance, le problème de la médiane a été démontré NP-difficile, même pour de petits ensembles ne contenant que 4 permutations. Je parlerai dans cet exposé de méthodes efficaces de réduction d’espace pour le problème général de même que d’un lien intéressant avec le 3-Hitting Set Problem dans le cas spécial où on s’intéresse à la médiane d’un ensemble 3 permutations. Les travaux présentés dans cet exposé ont été réalisés en collaboration avec Robin Milosz (Université de Montréal) et Adeline Pierrot (LRI, Université Paris-Sud).

Preuves, programmes et systèmes
Jeudi 28 février 2019, 10 heures 30, Salle 3052
François Bergeron (UQAM) Theory of species of structures and applications

Species of Structures, introduced almost 40 years ago, give a natural conceptu l framework for the notion of ``combinatorial construction on sets’’. Fundamental operations between species allow the specification of new species in terms of known ones, giving a systematic context for the solution of classical enumeration questions, including both labelled and unlabelled enumeration (a.k.a. Pólya Theory). In this talk, we will give an accessible introduction to the Theory of Species, with many illustrations. If time allows, we will also survey some of many areas (computer science, theoretical physics, chemistry, etc.) where they are currently useful.

Gâteau de l'IRIF
Jeudi 28 février 2019, 17 heures 30, in front of room 3052
Abhishek De, Alexandre Nolin, Robin Vacus, Rongxing Xu (IRIF CakeTM) Gâteau de l'IRIF

IRIF CakeTM is an amazing opportunity to meet people while simultaneously eating cakes baked by your fellow colleagues! Join us every Thursday, at 5pm, in front of room 3052 (Sophie Germain 3rd floor) for a weekly feast. You can also express your cooking skills and volunteer to bake a cake by sending an email to cake@irif.fr.

Algorithmes et complexité
Vendredi 1 mars 2019, 15 heures, Salle 1007
Jacob Leshno (Chicago Booth) Facilitating Student Information Acquisition in Matching Markets

We develop a tractable model for a matching market where students form preferences through costly information acquisition. As the market outcome consists of both an assignment as well as the acquired information, we study how the marketplace can direct both the allocation and the information acquisition process. We define regret-free stable outcomes, where the matching is stable under the partial preferences and each student has acquired information optimally, as if she were last to market; regret-free stable outcomes are optimal in settings where students make decentralized decisions about how to acquire information and can wait for more information. We show that regret-free stable outcomes always exist and can be characterized by cutoffs. However, we also show that regret-free stable outcomes cannot be discovered under practical restrictions – any discovery process can reach deadlocks where every student would like to wait for additional market information before acquiring information. Instead, historical information can facilitate the implementation of approximate regret-free stable outcomes, suggesting that an important role of matching markets is to aggregate information from multiple years. We also provide a method for bootstrapping information acquisition when historical information is not available.