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.

(rafraîchir la page pour changer de notion)

17.11.2018
Four papers coauthored by IRIF members will be presented at POPL’19, the main conference on programming languages and programming systems. The papers' topics are game semantics, proof theory, gradual typing, and consistency for concurrent computations.

Games are mathematical objects used for modeling situations in which several participants/players interact, and each of them aims at fulfilling a personal goal. Real games such as chess or go are cases in which there are two players which are opponent. Games occur in computer science for modeling the logical duality between conjunction and disjunctions, or for defining particular families of complexity classes. Games appear in verification for describing how a system has to react to the environment (the opponent) in order to perform what it has been designed for.
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.
Proof theory is the branch of mathematical logic that studies proofs as mathematical objects. In particular, proof are syntactic constructions built from axioms and inference rules. Relevant to computer science are the studies of computational and complexity aspects of proofs.
Memory consistency models characterize the effect of concurrent invocations to a library implementing a shared state, e.g., a queue or a key-value map. Strong consistency means that the results of concurrently-executed invocations match the results of some serial execution of those same invocations. Since strong consistency carries a significant penalty on performance, modern implementations provide weaker guarantees known as weak consistency models, e.g., eventual or causal consistency.

9.11.2018
The first session of a series of seminars Graph Theory in Paris will be hosted by IRIF. There will be two seminars by Monique Laurent and Lex Schrijver on November 23, at 2pm, in Amphi Turing of Sophie Germain building.

10.11.2018
The first meeting of the French-Chinese research project Verification Interaction Proof will take place in Paris at IRIF on November 19-24. Registration is free but mandatory.

20.11.2018
One paper coauthored by Laurent Feuilloley while he was PhD student at IRIF will be presented at SODA’19, the main conference in algorithm design. The paper provides lower bounds for the fundamental problem of text indexing with mismatches and differences using the Strong Exponential Time Hypothesis.

20.11.2018
Two papers coauthored by IRIF members will be presented at QIP’19, the main conference for theoretical quantum information research. Topics include efficient quantum algorithms for both algebraic and distributed problems.

19.11.2018
IRIF has the great pleasure to welcome Mahsa Shirmohammadi, researcher scientist (CNRS) from LIS, who is visiting IRIF for six months and who is an expert in the analysis and verification of timed, counter and probabilistic systems.

12.10.2018
IRIF has the great pleasure to welcome a new assistant professor (Paris Diderot): Adrien Guatto, an expert in synchronous languages, typed functional programming, and categorical semantics.

12.11.2018
IRIF and PCQC are partners in the EU Flagship project Quantum Internet Alliance (QIA) and in charge of delivering the QIA's blueprint for the future of quantum communications. The EU selected nineteen research projects, and ten of them are based on French teams.

Gâteau du jeudi - Thursday Cake
jeudi 22 novembre 2018, 17h30, in front of room 3052
Cédric Ho Thanh, Alessandro Luongo, Axel Osmond, Anupam Prakash, Matthieu Sozeau (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.

Combinatoire énumérative et analytique
jeudi 22 novembre 2018, 11h45, Salle 1007
Arthur Nunge (IRIF) An algebraic refinement of the 2-PASEP probabilities.

The Partially asymmetric exclusion process (PASEP) is a physical model viewed as a Markov chain representing the displacement of particles over a finite line. The steady-state probabilities of this chain can be computed by enumerating permutations according to certain statistics. These probabilities have a natural connexion with some transition matrices, in the algebra of noncommutative symmetric functions, which implies a refinement of the probabilities of the PASEP using statistics on permuations. We place ourself in the context of the 2-PASEP, the PASEP with two kind of particles, and exhibit a connexion with the free algebra indexed by segmented compositions using statistics on partially signed permutations.

Preuves, programmes et systèmes
jeudi 22 novembre 2018, 10h30, Salle 3052
Stéphane Graham-Lengrand (LIX, CNRS) The intuitionistic calculus that was discovered 6 times

In this talk I will review G4ip, a simple calculus for intuitionistic propositional logic (IPL) that provides a decision procedure for provability. Its basic mechanisms can be traced back to Vorob'ev in the 50s, and were found again by Hudelmaier (88), Dyckhoff (90), Paulson (91), and (with a linear logic flavour) Lincoln-Scedrov-Shankar (91). In 2015, Claessen and Rosén presented the fastest decision procedure for IPL, based on SMT-solving techniques. We describe their algorithm and show how it can be seen as a variant of the aforementioned calculus, albeit with key variations that provide increased performance. Their algorithm relies on a SAT-solver used as a black box and treats intuitionistic entailment as a theory. We show how the recent framework of model-constructing satisfiability for SMT-solving could further integrate intuitionistic reasoning within the main SAT-solving loop. This would constitute an intuitionistic variant of the main algorithm of SAT-solvers, where Kripke models are built instead of Boolean models.

Algorithmes et complexité
jeudi 22 novembre 2018, 14h00, Salle 1007
Aviad Rubinstein (Stanford) Distributed PCP Theorems for Hardness of Approximation in P

We present a new model of probabilistically checkable proof (PCP), which we call “Distributed PCP”: A satisfying assignment (x in {0,1}^n) to a SAT instance is shared between two parties (Alice knows x_1, … x_{n/2}, and Bob knows x_{n/2+1},…,x_n). Their goal is to jointly write a PCP for x, while exchanging little or no information.

Using our new framework, we obtain, for the first time, PCP-like hardness of approximation results for problems in P.

Based on joint works with Amir Abboud, Lijie Chen, Shafi Goldwasser, Kaifeng Lyu, Guy Rothblum, and Ryan Williams.

Automates
vendredi 23 novembre 2018, 14h30, Salle 3052
Sébastien Labbé (IRIF) Structure substitutive des pavages apériodiques de Jeandel-Rao

En 2015, Jeandel et Rao ont démontré par des calculs exhaustifs faits par ordinateur que tout ensemble de tuiles de Wang de cardinalité ≤ 10 soit admettent un pavage périodique du plan Z² soit n'admettent aucun pavage du plan. De plus, ils ont trouvé un ensemble de 11 tuiles de Wang qui pavent le plan mais jamais de façon périodique. Dans cet exposé, nous présenterons une définition alternative des pavages apériodiques de Jeandel-Rao comme le codage d'une Z²-action sur le tore et nous décrivons la structure substitutive de ces pavages.

Soutenances d'habilitation
vendredi 23 novembre 2018, 14h00, Salle 234C, Halle aux Farines
Christine Tasson (IRIF) Sémantiques des Calculs Distribués, Différentiels et Probabilistes

Depuis les années 60, la sémantique s'est avérée très utile pour introduire des langages de haut niveau permettant d'écrire des programmes complexes et de les comprendre à un niveau mathématique précis. Dans les années 80, la logique linéaire a été introduite par Girard, reflétant des propriétés sémantiques liées à l'utilisation des ressources. Cette direction a été poursuivie par Ehrhard dans les années 2000 avec l'introduction du lambda-calcul différentiel. Dans ces modèles, les programmes sont approximés par des polynômes, dont les monômes représentent les appels d'un programme à ses entrées lors de son exécution. Cette approche analytique a constitué un outil crucial pour l'étude des propriétés quantitatives apparaissant dans les langages de programmation probabiliste. En parallèle, depuis les années 90, plusieurs modèles géométriques ont été développés pour représenter des traces d'exécution dans les systèmes distribués. Dans cette thèse d'habilitation, nous présentons des modèles que nous avons étudiés dans ces trois domaines : les systèmes distribués, le lambda-calcul différentiel, la programmation probabiliste, ainsi que les techniques générales nécessaires et les résultats qu'ils nous ont permis d'obtenir. Celles-ci ont nécessité l'utilisation et le développement d'outils issus de la combinatoire, de la topologie dirigée, de l'analyse fonctionnelle, de la théorie des catégories et des probabilités.

Soutenances de thèses
vendredi 23 novembre 2018, 14h00, Laboratoire MAP5, 45 rue des Saint-pères, 7eme étage, salle du conseil
Léo Planche (IRIF) Décomposition de graphes en plus courts chemins et en cycles de faible excentricité

En collaboration avec des chercheurs en biologie à Jussieu, nous étudions des graphes issus de données biologiques afin de d'en améliorer la compréhension. Ces graphes sont constitués à partir de fragments d'ADN, nommés reads. Chaque read correspond à un sommet, et deux sommets sont reliés si les deux séquences d'ADN correspondantes ont un taux de similarité suffisant. Ainsi se forme des graphes ayant une structure bien particulière que nous nommons hub-laminaire. Un graphe est dit hub-laminaire s'il peut être résumé en quelques plus courts chemins dont tous les sommets du graphe soient proche. Nous étudions en détail le cas où le graphe est composé d'un unique plus court chemin d'excentricité faible. Nous améliorons la preuve d'un algorithme d'approximation déjà existant et en proposons un nouveau, effectuant une 3-approximation en temps linéaire. De plus, nous analysons le lien avec le problème de k-laminarité défini par Michel Habib et Finn Völkel, ce dernier consistant en la recherche d'un diamètre de faible excentricité. Nous étudions ensuite le problème du cycle isométrique de plus faible excentricité. Nous montrons que ce problème est NP-complet et proposons deux algorithmes d'approximations. Nous définissons ensuite précisément la structure “hub-laminaire” et présentons un algorithme d'approximation en temps O(nm). Nous confrontons cet algorithme à des graphes générés par une procédure aléatoire et l'appliquons à nos données biologiques. Pour finir nous montrons que le calcul du cycle isométrique d'excentricité minimale permet le plongement d'un graphe dans un cercle avec une distorsion multiplicative faible. Le calcul d'une décomposition hub-laminaire permet quant à lui une représentation compacte des distances avec une distorsion additive bornée.

Vérification
lundi 26 novembre 2018, 11h10, Salle 1007
Matthias Függer (LSV - CNRS & ENS de Cachan) Fast Asymptotic and Approximate Consensus in Highly Dynamic Networks

Agreeing on a common value in a distributed system is a problem that lies at the heart of many distributed computing problems and occurs in several flavors. Unfortunately, even modest network dynamics already prohibit solvability of exact consensus, where agents have to decide on a single output value that is within the range of the agents' initial values.

For many problems (distributed control, clock synchronization, load balancing, …) it is however sufficient to asymptotically converge to the same value, or decide on values not too far from each other. We study solvability of these consensus variants in highly dynamic networks, provide time complexity results, and present fast algorithms. We then show how the results on dynamic networks are relevant for classical fault-models, such as asynchronous message passing with crashes.

The talk is on previous and current research with Bernadette Charron-Bost (LIX), Thomas Nowak (LRI), and Manfred Schwarz (ECS, TU Wien).

Sémantique
lundi 26 novembre 2018, 14h00, Salle 3052
Hendrik Maarand (Tallinn University of Technology) Derivatives of Existentially Regular Trace Languages

We provide syntactic (expression-level) language derivative operations, both in the styles of Brzozowski and Antimirov, for trace closures of regular word languages wrt. an independence relation on the alphabet. The Brzozowski and Antimirov style derivatives essentially define functional resp. relational small-step operational semantics of an (abstracted) sequential programming language where some instructions, given by the independence relation, can be reordered without any observable consequences. Our development is motivated by the fact that some aspects of relaxed memories can be explained by allowing the threads of a concurrent program to be reordered in this manner.

Algorithmes et complexité
mardi 27 novembre 2018, 11h00, Salle 1007
Sagnik Mukhopadhyay (Computer Science Institute of Charles University) Lifting theorems for Equality

We show a deterministic simulation (or lifting) theorem for composed problems $f \circ \EQ_n$ where the inner function (the gadget) is Equality on $n$ bits. When $f$ is a total function on $p$ bits, it is easy to show via a rank argument that the communication complexity of $f\circ \EQ_n$ is $\Omega(\deg(f) \cdot n)$. However, there is a surprising counter-example of a partial function $f$ on $p$ bits, such that any completion $f'$ of $f$ has $\deg(f') = \Omega(p)$, and yet $f \circ \EQ_n$ has communication complexity $O(n)$. Nonetheless, we are able to show that the communication complexity of $f \circ \EQ_n$ is at least $D(f) \cdot n$ for a complexity measure $D(f)$ which is closely related to the $\AND$-query complexity of $f$ and is lower-bounded by the logarithm of the leaf complexity of $f$. As a corollary, we also obtain lifting theorems for the set-disjointness gadget, and a lifting theorem in the context of parity decision-trees, for the $\NOR$ gadget.

In this talk, I will talk about simulations or lifting theorems in general from a previous work of Chattopadhyay et al., and lifting theorem for Equality in particular—especially why the general recipe of Chattopadhyay et al. does not work for Equality. I will also mention an application of this technique to prove tight communication lower bound for Gap-Equality problem. This is a joint work with Bruno Loff.