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

## Notion du jour

(*rafraîchir la page pour changer de notion*)

## Actualités

*15.06.2018*

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.

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

*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”*.

*06.06.2018*

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

*01.06.2018*

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.

*30.05.2018*

**« 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.

*25.05.2018*

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.

*21.05.2018*

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.

*13.05.2018*

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.

*11.05.2018*

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

*27.02.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.

## Événements

Vérification

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.

Automates

vendredi 22 juin 2018, 14h30, Salle 3052

**Johanna Ochreniak** (IRIF) *tba*

tba

Vérification

lundi 25 juin 2018, 11h00, Salle 3052

**Nicolas Jeannerod** (IRIF) *Deciding the First-Order Theory of an Algebra of Feature Trees with Updates*

tba