## Bienvenue à l'IRIF

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 objectifs scientifiques de l'IRIF se situent au cœur de l'informatique, se focalisant sur la conception, l'analyse, la preuve et la vérification d'algorithmes et de programmes, appuyé sur des recherches fondamentales en combinatoire, théorie des graphes, logique, théorie des automates, etc.

L'IRIF regroupe près de 170 personnes. Six de ses membres ont été lauréats de l'European Research Council (ERC), et deux sont membres de l'Institut Universitaire de France (IUF).

## Actualités

*11.01.2018*

January the 10th 2018, this is the kick-off meeting of the ANR project FREDDA (FoRmal mEthods for the Design of Distributed Algorithms).

*09.01.2018*

In 2018, two faculty positions are opened at IRIF: one full professor position,
and one teaching assistant position.

*05.01.2018*

Lucas Boczkowski and Amos Korman from IRIF, with their co-authors, will present at ITCS 2018 a non-conditional lower bound on information dissemination in stochastic populations. The paper is the first ever to combine an algorithmic lower bound with a biology experiment in collective behavior.
https://arxiv.org/pdf/1712.08507

*19.12.2017*

IRIF and ATOS have started the first Industrial PhD Thesis (CIFRE) on quantum algorithms in France.
The PhD candidate Alessandro Luongo is co-advised by Iordanis Kerenidis and Frédéric Magniez.

*08.12.2017*

Ludovic Patey was awarded the Prix Thiessé de Rosemont / Demassieux for his PhD thesis « Les mathématiques à rebours de théorèmes de type Ramsey », supervised by Laurent Bienvenu and Hugo Herbelin.

*29.11.2017*

Amina Doumane was awarded the Gilles Kahn prize for her PhD thesis entitled « On the infinitary proof theory of logics with fixed points » supervised by Alexis Saurin, David Baelde and Pierre-Louis Curien.

*29.11.2017*

Wenjie Fang was awarded the Honorable Mention of the Gilles Kahn prize for his
PhD thesis entitled « Aspects énumératifs et bijectifs des cartes combinatoires : généralisation, unification et application » and supervised by Guillaume Chapuy and Mireille Bousquet-Mélou.

*27.11.2017*

Scientific Day in memory of Maurice Nivat, professor at Paris Diderot University and a pionneer of thoeretical computer science in France and in the world, who passed away on September the 21st, 2017.

*15.11.2017*

IRIF is happy to host and organize the 59th IEEE Symposium on Foundations of Computer Science (FOCS 2018), at Maison de la Chimie, Paris, October 07-09, 2018.

*06.10.2017*

Guillaume Lagarde and Sylvain Perifel have solved a 20-year old conjecture related to Lempel-Ziv. This will be presented at the
29th ACM-SIAM Symposium on Discrete Algorithms (SODA 2018).

*01.09.2017*

IRIF has the great pleasure to welcome a new assistant professor: Bérénice Delcroix-Oger, an expert in combinatorics and computational algebra.

*15.06.2017*

Victor Lanvin is awarded the first prize for the ACM Student Research Competition Grand Finals, undergraduate category. The prize will be presented on June the 24th at the *Turing Award* Cerimony in San Francisco.

## Événements

Algorithmes et complexité

mercredi 17 janvier 2018, 11h00, Salle 3014

**Philip Lazos** (Oxford) *The Infinite Server Problem*

We study a variant of the k-server problem, the infinite server problem, in which infinitely many servers reside initially at a particular point of the metric space and serve a sequence of requests. In the framework of competitive analysis, we show a surprisingly tight connection between this problem and the (h,k)-server problem, in which an online algorithm with k servers competes against an offline algorithm with h servers. Specifically, we show that the infinite server problem has bounded competitive ratio if and only if the (h,k)-server problem has bounded competitive ratio for some k=O(h). We give a lower bound of 3.146 for the competitive ratio of the infinite server problem, which implies the same lower bound for the (h,k)-server problem even when k/h→∞ and holds also for the line metric; the previous known bounds were 2.4 for general metric spaces and 2 for the line. For weighted trees and layered graphs we obtain upper bounds, although they depend on the depth. Of particular interest is the infinite server problem on the line, which we show to be equivalent to the seemingly easier case in which all requests are in a fixed bounded interval away from the original position of the servers. This is a special case of a more general reduction from arbitrary metric spaces to bounded subspaces. Unfortunately, classical approaches (double coverage and generalizations, work function algorithm, balancing algorithms) fail even for this special case.

Théorie des types et réalisabilité

mercredi 17 janvier 2018, 14h00, Salle 1007

**Rodolphe Lepigre** () *Practical Curry-Style using Choice Operators, Local Subtyping and Circular proofs*

In a recent (submitted) work with Christophe Raffalli, we designed a rich type system for an extension of System F with subtyping. It includes primitive sums and products, existential types, (co-)inductive (sized) types, and it supports general recursion with termination checking. Despite its Curry-style nature, the system can be (and has been) implemented thanks to new techniques based on choice operators, local subtyping and circular proofs. During the talk, I will give you a flavour of these three ideas. In particular, I will show how choice operators can be used to get rid of free variables (and thus typing contexts), while yielding a clear semantics. I will show how local subtyping can be used to make the system syntax-directed. And I will show how circular proofs may be used to handle (co-)inductive types and (terminating) recursion.

References and links: - paper: http://lepigre.fr/files/docs/lepigre2017_subml.pdf - implementation of the system: https://github.com/rlepigre/subml - online interpreter and examples: https://rlepigre.github.io/subml

Sémantique

mercredi 17 janvier 2018, 10h00, Salle 3052

**Luc Pellissier** (ENS Lyon) *Intersection Types, Linear Approximations and the Grothendieck construction*

Intersection Types are a well-known family of tools that characterise different notions of normalisation. We develop a general framework for building such systems from a notion of approximation, that allows to recover many well-known intersection type systems, as well as new systems, for every calculus that can be translated into linear logic. This construction uses in a crucial way Melliès and Zeilberger’s “type systems as functors” viewpoint, as well as an adapted Grothendieck construction.

Based on a joint work with Damiano Mazza and Pierre Vial.

Sémantique

mercredi 17 janvier 2018, 11h00, Salle 3052

**Soichiro Fujii** (National Institute of Informatics (NII, Tokyo)) *A unified framework for notions of algebraic theory*

Universal algebra uniformly captures various algebraic structures, by expressing them as equational theories or (abstract) clones. The ubiquity of algebraic structures in mathematics has also given rise to several variants of universal algebra, such as symmetric and non-symmetric operads, clubs, and monads. In this talk, I will present a unified framework for these cousins of universal algebra, or notions of algebraic theory.

First I will explain how each notion of algebraic theory can be identified with a certain monoidal category, in such a way that theories correspond to monoids. Then I will introduce a categorical structure underlying the definition of models of theories. In specific examples, it often arises in the form of oplax action or enrichment. Finally I will uniformly characterize categories of models for various notions of algebraic theory, by a double-categorical universal property in the pseudo-double category of profunctors.

Automates

vendredi 19 janvier 2018, 14h30, Salle 3058

**Verónica Becher** (Universidad de Buenos Aires) *tba*

tba

Vérification

lundi 22 janvier 2018, 11h00, Salle 1007

**Josef Widder** (TU Wien) *Synthesis of Distributed Algorithms with Parameterized Thresholds Guards*

Fault-tolerant distributed algorithms are notoriously hard to get right. I present an automated method that helps in that process: the designer provides specifications (the problem to be solved) and a sketch of a distributed algorithm that keeps arithmetic details unspecified. Our tool then automatically fills the missing parts. In particular, I will consider threshold-based distributed algorithms, where a process has to wait until the number of messages it receives reaches a certain threshold, in order to perform an action. Such algorithms are typically used for achieving fault tolerance in distributed algorithms for broadcast, atomic commitment, or consensus. Using this method, one can synthesize distributed algorithms that are correct for every number n of processes and every number t of faults, provided some resilience condition holds, e.g., n > 3t. This approach combines recent progress in parameterized model checking of distributed algorithms—which I also address—with counterexample-guided synthesis.

This is joint work with Marijana Lazić, Igor Konnov, and Roderick Bloem.

Algorithmes et complexité

mardi 23 janvier 2018, 10h00, Collège de France, Amphithéâtre Maurice Halbwachs - Marcelin Berthelot

**Claire Mathieu - Tim Roughgarden** (DI ENS, IRIF - Stanford University) *On Game Theory Through the Computational Lens*

Seventh lecture from Claire Mathieu at Collège de France on Algorithms (at 10am), followed by a talk from Tim Roughgarden on Game Theory Through the Computational Lens (at 11am).

Additional information: http://www.college-de-france.fr/site/claire-mathieu/course-2018-01-23-10h00.htm

Séminaire des doctorants

mercredi 24 janvier 2018, 11h00, Salle 3052

**Alessandro Luongo And Ny Aina Andriambolamalala** (Algorithms and complexity team and Combinatorics team) *TBA and TBA*

TBA and TBA