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, et plus particulièrement sur la conception, l'analyse, la preuve et la vérification d'algorithmes, de programmes et de langages de programmation. Ils s'appuient sur des recherches fondamentales développées à l'IRIF en combinatoire, graphes, logique, automates, types, sémantique et algèbre.

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


Pierre Vial (IRIF) will present at LICS 2018 an excerpt of his PhD work at IRIF proving that every lambda-term has an infinite linear representation in the infinitary relational model. This work pioneers a technique that allows giving a semantic even to unproductive programs.


Paul-André Melliès (IRIF) will present at LICS 2018 his work on ribbon tensorial logic, a primary logic designed to reveal the secret topology of reasoning. This is the first time that logical proofs are faithfully translated into topological tangles using functorial knot theory.


Amos Korman (IRIF) Amos Korman is co-chairing, and organizing the 6th Workshop on Biological Distributed Algorithms, to be held in London in July, the 23rd.

Institut de France

Miklos Santha (IRIF) participates to the conference-debate « Calcul, communication, simulation et métrologie quantiques : des principes aux réalisations concrètes » to be held the 15 May in the Institut de France (23, quai de Conti, 75006 Paris).


IRIF is proud to announce that Delia Kesner, professor of University Paris Diderot and researcher at IRIF, was appointed senior member of IUF.


Six papers coauthored by IRIF members will be presented at the prestigious conference LICS'18 in Oxford this summer. Topics range from λ-calculus, to Separation Logic…


Victor Lanvin (PhD student of Giuseppe Castagna, IRIF) is awarded the Google PhD fellowship! Through the FSMP, Google will give a significant support to Victor's research work.

Numeration 2018

The conference Numeration 2018 will be held on May 22-25 at the Univerity Paris Diderot, and is organized by Valérie Berthé, Christiane Frougny and Wolfgang Steiner from IRIF.


“The Kappa platform for rule-based modeling”, a collaboration between Jean Krivine (IRIF) and researchers from Harvard University, ENS and Santa Cruz University will be presented at ISMB2018.


Adrian Kosowski (IRIF), together with Bartek Dudek (University of Wroclaw), will present at STOC 2018 a new protocol for spreading information in a population. This is the first time that methods of oscillatory dynamics are used to solve a basic task of information dissemination.


Constantin Enea (IRIF) is an organizer of the 2018 edition of the EPIT research school, on the subject of software verification, to he held in Aussois on May 7-11 2018.


Peter Habermehl (IRIF) and Benedikt Bollig (LSV, ENS Paris-Saclay) organize the research school MOVEP (Modelling and Verification of Parallel Processes), from on July 16-20 in Cachan.

mardi 22 mai 2018, 14h00, Salle 1007
François Pirot (Université de Strasbourg) Fractional chromatic number of small degree graphs and girth.

It is well known that you can color a graph G of maximum degree d greedily with d+1 colors. Moreover, this bound is tight, since it is reached by the cliques. Johansson proved with a pseudo-random coloring scheme that you can color triangle-free graphs of maximum degree d with no more than O(d/log d) colors. This result has been recently improved to (1+ε)(d/log d) for any ε>0 when d is big enough. This is tight up to a multiplicative constant, since you can pseudo-randomly construct a family of graphs of maximum degree d, arbitrary large girth, and chromatic number bigger than d / (2 log d). Although these are really nice results, they are only true for big degrees, and there remains a lot to say for small degree graphs. When the graphs are of small degree, it is interesting to consider the fractional chromatic number instead, since it has infinitely many possible values – note that cubic graphs are either bipartite, the clique K4, or of chromatic number 3. It has already been settled that the maximum fractional chromatic number over the triangle-free cubic graphs is 14/5. I will present a systematic method to compute upper bounds for the independence ratio of graphs of given (small!) degree and girth, which can sometimes lead to upper bounds for the fractional chromatic number, and can be adapted to any family of small degree graphs under some local constraints.

Algorithmes et complexité
mardi 22 mai 2018, 11h00, Salle 1007
Anupam Prakash (IRIF) Improved quantum linear system solvers and applications to machine learning

I will describe recent results in the QRAM model that improve the sparsity dependance for quantum linear system solvers to \mu(A) = \min (||A||_F, ||A||_1) where ||A||_1 is the maximum l-1 norm of the rows and columns of A and ||A||_F is the Frobenius norm. These results achieve a worst case quadratic speedup over the HHL algorithm and its improvements and exponential speedups for some cases. I will also present some applications of the improved linear system solvers to quantum machine learning.

Séminaire des doctorants
mercredi 23 mai 2018, 11h00, Salle 3052
Léo Stefanesco (Algebra and calculus, proofs and programs teams) An Asynchronous Soundness Theorem for Concurrent Separation Logic

The talk will start with an introduction to (concurrent) separation logic.


Concurrent separation logic (CSL) is a specification logic for concurrent imperative programs with shared memory and locks. In this talk, we develop a concurrent and interactive account of the logic inspired by asynchronous game semantics. To every program C, we associate a pair of asynchronous transition systems [C]S and [C]L which describe the operational behavior of the Code when confronted to its Environment, both at the level of machine states (S) and of machine instructions and locks (L). We then establish that every derivation tree π of a judgment Γ ⊢ {P}C{Q} defines a winning and asynchronous strategy [π] with respect to both asynchronous semantics [C]S and [C]L. From this, we deduce an asynchronous soundness theorem for CSL, which states that the canonical map L : [C]S → [C]L from the stateful semantics [C]S to the stateless semantics [C]L satisfies a basic fibrational property. We advocate that this fibrational property provide a clean and conceptual explanation for the usual soundness theorem of CSL, including the absence of data races.

(Joint work with Paul-André Melliès)

Catégories supérieures, polygraphes et homotopie
vendredi 25 mai 2018, 14h00, Salle 1007
Martin Szyld (Université de Buenos Aires) The homotopy relation in a category with weak equivalences

I will present the results of the article (arXiv:1804.04244) which deals with the classical construction of the homotopy category of a model category (which is done by performing a quotient of the arrows by the homotopy relation) in the context of categories with weak equivalences. By studying this situation in an abstract context, one can define a relation of homotopy “only with respect to the weak equivalences” which yields the desired localization and coincides with the classical one for model categories. As it is usually the case, the proofs of these results, which consider only a family of arrows instead of three, become simpler. In particular, they allowed a generalization to bicategories in a current work with E. Descotte and E. Dubuc, which I will present too if time permits.

vendredi 25 mai 2018, 14h30, Salle 3052
Ulrich Ultes-Nitsche (University of Fribourg) A Simple and Optimal Complementation Algorithm for Büchi-Automata

In my presentation, I am going to present joint work with Joel Allred on the complementation of Büchi automata. When constructing the complement automaton, a worst-case state-space growth of O((0.76n)^n) cannot be avoided. Experiments suggest that complementation algorithms perform better on average when they are structurally simple. We develop a simple algorithm for complementing Büchi automata, operating directly on subsets of states, structured into state-set tuples, and producing a deterministic automaton. Then a complementation procedure is applied that resembles the straightforward complementation algorithm for deterministic Büchi automata, the latter algorithm actually being a special case of our construction. Finally, we prove our construction to be optimal, i.e. having an upper bound in O((0.76n)^n), and furthermore calculate the 0.76 factor in a novel exact way.

lundi 28 mai 2018, 11h00, Salle 1007
Ana Sokolova (Universität Salzburg, Austria) Linearizability of Concurrent Data Structures via Order Extension Theorems

The semantics of concurrent data structures is usually given by a sequential specification and a consistency condition. Linearizability is the most popular consistency condition due to its simplicity and general applicability. Verifying linearizability is a difficult, in general undecidable, problem.

In this talk, I will discuss the semantics of concurrent data structures and present recent order extension results (joint work with Harald Woracek) that lead to characterizations of linearizability in terms of violations, a.k.a. aspects. The approach works for pools, queues, and priority queues; finding other applications is ongoing work. In the case of pools and queues we obtain already known characterizations, but the proof method is new, elegant, and simple, and we expect that it will lead to deeper understanding of linearizability.

Algorithmes et complexité
mardi 29 mai 2018, 11h00, Salle 1007
Steve Alpern (University of Wariwick, UK) Shortest Paths in Networks with Unreliable Directions

The work of Korman and others, based on investigations of navigational techniques of ‘crazy ants’, leads to the following problem: Let Q be a network with given arc lengths, and let H be a ‘home’ node. At each node a permanent direction is given (one of the adjacent arcs) which leads to a shortest path path from that node to H with probability p less than one. Starting from a node S, a searcher chooses the given direction at each reached node with probability q; otherwise he chooses randomly. He arrives home at node H in expected time T=T(S,H,p,q). How should q be chosen to minimize T? Perhaps when reaching a node the searcher sees its degree k so chooses the given direction with probability q(k). Related problems have been studied for tree from a graph theoretical perspective.