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).

(rafraîchir la page pour changer de notion)

Amina Doumane

Amina Doumane (former PhD student at IRIF, now at LIP) was awarded the Ackermann prize of EACSL for her PhD thesis entitled On the infinitary proof theory of logics with fixed points.

TYPES 06.06.2018
Delia Kesner (IRIF) and Matthieu Sozeau (IRIF) will both give invited talks entitled “Multi Types for Higher-Order languages” and “The Predicative, Polymorphic Calculus of Cumulative Inductive Constructions and its implementation” at TYPES 2018, held in Braga (Portugal), June 18-21.

IRIF distinguished talk 06.06.2018
We are delighted to host as part of our IRIF Distinguished Talks Series Christos Papadimitriou (Columbia University) on July 13, 10:30 for a talk entitled “A computer scientist thinks about the Brain”.

Software Heritage

Today Roberto Di Cosmo (professor at IRIF) with a ceremony at UNESCO opened to the public the archives of Softwareheritage.org, a worldwide initiative to create a universal library of computer programme source codes since the dawn of the digital age. .

Collège de France

Claire Mathieu (IRIF associate member) organizes a 1-day colloquium on Approximation algorithms and networks at Collège de France on June 7. This is part of the Chair in Informatics and Computational Sciences at College de France in association with INRIA.
approximation algorithm

The approximation algorithms are algorithms that produce a solution that approximates the best possible solution of an optimization problem. While finding the optimal solution of practical problems is often infeasible, an approximation algorithm usually produces its solution in an efficient way and provides formal guarantees about the quality of the approximation. An example of such a problem is the so-called “traveling salesman problem” which consists in finding among all possible itineraries the shortest route that allows a salesman to visit a given set of cities and come back home.
Informatique & sciences du numérique

« Tous femmes de numérique ! » Après leur rencontre avec 4 informaticiennes de l’IRIF, 14 lycéennes du Lycée Jules Ferry ont expliqué à leurs camarades l’exposition permanente du Palais de la découverte sur l’informatique et les sciences du numérique le 29/05.


Marie Kerjean (PhD student IRIF) will present at LICS 2018 a logical account for linear partial differential equations. With this work, she unveils a bridge between mathematical physics and proof theory, paving the way for exciting and mutually beneficial transfers of techniques.

A sequent represents a theorem by a sequence of hypotheses and the sequence of possible theses they imply. This formalism underlines a symmetry hypotheses/theses ruled by negation and is used in sequent calculus to formalise proofs and to study their properties.

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.

A part of a program is unproductive if it performs an infinite number of computing steps without any interaction with the rest of the program or external devices. Unproductive code is basically useless, and may even be unsafe, and detecting parts of code that are unproductive is important to improve software quality.

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.
knot theory

Knot theory studies mathematical knots. These are like the usual shoelaces and rope knots but with the difference that the ends of the string are joined together so that it cannot be undone. Of particular interest is the study of when two knots are equivalent, that is when one can be transformed into the other without cutting the string or passing the string through itself. The theory has applications in physics, biology, chemistry, and computer science. For instance, the security of some quantum money relies on the assumption that given two different looking but equivalent knots, it is difficult to explicitly find a transformation that takes one to the other.

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.
biological algorithm

Biological algorithm is a term used to describe the biological processes from an algorithmic, or computer scientific, perspective. It concerns questions such as what are the algorithmic challenges faced by the biological organism, and what are the algorithmic principals used in order to overcome these challenges. For example, when a group of ants finds a large piece of food and needs to decide its navigation rout back to the nest, what are the benefits and pitfalls of noise in their communication?

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.

lundi 18 juin 2018, 11h00, Salle 1007
Eugène Asarin (IRIF) Distance on timed words and applications

We introduce and study a new (pseudo) metric on timed words having several advantages:

- it is global: it applies to words having different number of events;

- it is realistic and takes into account imprecise observation of timed events; thus it reflects the fact that the order of events cannot be observed whenever they are very close to each other;

- it is suitable for quantitative verification of timed systems: we formulate and solve quantitative model-checking and quantitative monitoring in terms of the new distance, with reasonable complexity;

- it is suitable for information-theoretical analysis of timed systems: due to its pre-compactness the quantity of information in bits per time unit can be correctly defined and computed.

(Joint work with Nicolas Basset and Aldric Degorre)

Algorithmes et complexité
mardi 19 juin 2018, 11h00, Salle 1007
Leonard Wossnig (University College London) Sketching as tool for faster quantum simulation

Following the works of Drineas et al. (2004), Randomised Numerical Linear Algebra (RNLA) applications have enjoyed a increasing surge of interest in the classical algorithms community. Following their success we recently demonstrated a classical algorithm based on the Nystroem method which allows us to efficiently simulate dynamics of quantum system with specific structural conditions. We briefly introduce the most basic RNLA algorithm by Drineas et al. to give an overview of the topic and then outline our own recent work. We follow with a discussion of potential application of related methods, including spectral sparsification, in quantum algorithms for Hamiltonian Simulation and quantum linear systems; We finish with a short description of own current work related to spectral sparsification (Spielmann & Teng 2011) for Hamiltonian simulation.

Séminaire des doctorants
mercredi 20 juin 2018, 11h00, Salle 3052
Laurent Feuilloley (Équipes Compsys, GANG et graphes) Distributed decision

In this talk, I will introduce the domain of distributed decision, and review some of the results and insights gathered during my PhD.

The underlying model of this study is the local model. The local model is defined to answer questions of the following type: given a communication network, whose nodes are machines, and edges are communication links, is it possible that the nodes solve some task X, if they communicate only with the nodes that are close to them? A classic problem is colouring: can a node choose a colour, with only the knowledge of a small neighbourhood of the graph, such that the colours chosen by the nodes form a proper colouring of the graph? As in the centralized setting, it is interesting to study decision problems, that are yes-no questions, and to define complexity classes to classify these problems; this is distributed decision.

The complexity class we use as the equivalent of the class P in the centralized setting, is pretty small, and it is then natural to look at some form of non-determinism, to have a chance to understand more problems. In this model, non-determinism can be thought as a piece of global information that can be verified locally. The theoretical motivation is that to understand how local a problem is, one can ask how much global information is needed to solve it. The more practical motivation is that if one can design schemes with little global information then it can help to design more robust distributed algorithms such as self-stabilizing algorithms. The results I will present play with different natural notions of non-determinism, and how they influence the complexity classes defined.

I will spend time to carefully describe the model, thus no prior knowledge is needed.

Combinatoire énumérative et analytique
jeudi 21 juin 2018, 11h45, Salle 1007
Laurent Viennot (IRIF et INRIA) Revisiting Radius, Diameter, and all Eccentricity Computation in Graphs through Certificates

We introduce notions of certificates allowing to bound eccentricities in a graph. In particular , we revisit radius (minimum eccentricity) and diameter (maximum eccentricity) computation and explain the efficiency of practical radius and diameter algorithms by the existence of small certificates for radius and diameter plus few additional properties. We show how such computation is related to covering a graph with certain balls or complementary of balls. We introduce several new algorithmic techniques related to eccentricity computation and propose algorithms for radius, diameter and all eccentricities with theoretical guarantees with respect to certain graph parameters. This is complemented by experimental results on various real-world graphs showing that these parameters appear to be low in practice. We also obtain refined results in the case where the input graph has low doubling dimension, has low hyperbolicity, or is chordal.

vendredi 22 juin 2018, 14h30, Salle 3052
Johanna Ochreniak (IRIF) tba


lundi 25 juin 2018, 11h00, Salle 1007
Nicolas Jeannerod (IRIF) Deciding the First-Order Theory of an Algebra of Feature Trees with Updates