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

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.

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

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

Collège de France

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

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.

BDA

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

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érification
lundi 25 juin 2018, 11h00, Salle 3052
Nicolas Jeannerod (IRIF) Deciding the First-Order Theory of an Algebra of Feature Trees with Updates

The CoLiS project aims at applying techniques from deductive program verification and analysis of tree transformations to the problem of analyzing shell scripts. The data structure that is manipulated by these scripts, namely the file system tree, is a complex one.

We plan to use feature trees as an abstract representation of file system tree transformations. We thus investigate an extension of these feature trees that includes the update operation, which expresses that two trees are similar except in a particular subtree where there might have been changes.

We show that the first-order theory of this algebra is decidable via a weak quantifier elimination procedure which is allowed to swap existential quantifiers for universal quantifiers.

Combinatoire énumérative et analytique
mardi 26 juin 2018, 11h00, Salle 1007
Juanjo Rué (Universitat Politècnica de Catalunya) Enumeration of labelled 4-regular planar graphs

We present the first combinatorial scheme for counting labelled 4-regular planar graphs through a complete recursive decomposition. More precisely, we show that the exponential generating function of labelled 4-regular planar graphs can be computed effectively as the solution of a system of equations, from which the coefficients can be extracted. As a byproduct, we also enumerate labelled 3-connected 4-regular planar graphs, and simple 4-regular rooted maps. Finally, we discuss how to obtain asymptotic results.

This is based on joint works with Marc Noy (UPC) and Clément Réquile (TU Wien)

Séminaire des doctorants
mercredi 27 juin 2018, 11h00, Salle 3052
Victor Lanvin (Équipes Preuves, programmes, et Systèmes) Introduction to gradual typing with union and intersection types

Since the advent of types in programming languages, the two concepts of static typing and dynamic typing have been engaged in a terrible battle. Simply querying “static typing vs dynamic typing” yields more than half a million results on Stack Overflow. On the one hand, static typing provides strong safety guarantees before a program is even executed, by checking during compilation that types are not misused. On the other hand, dynamic typing is more flexible and is better suited to rapid prototyping. With both approaches having strong arguments in their favor, the battle seems endless. Yet, all hope is not lost. Gradual typing is a recent approach that aims at combining the safety guarantees of static typing with the flexibility and development speed of dynamic typing. The idea behind it is to introduce an “unknown” type, used to inform the compiler that additional type checks may need to be performed at run time in some places. Programmers can then “gradually” add type annotations to a program, and control precisely how much checking is done statically versus dynamically. Our work aims at integrating union and intersection types with gradual typing to allow for stronger safety guarantees and a finer control over dynamic types.

Note: this will (should) be a very general presentation about gradual typing and set-theoretic types consisting mostly of practical examples and without too many technical details. Don't hesitate to bring your computer, a book, or your Nintendo Switch™ if you already know the topic. :-)

Preuves, programmes et systèmes
jeudi 28 juin 2018, 10h30, Salle 3052
Olivier Hermant (CRI, Mines ParisTech) Intersection Types in Deduction Modulo Theory

In a 2012 paper, Richard Statman exhibited an inference system, based on second order monadic logic and non-terminating rewrite rules, that exactly types all strongly normalizable lambda-terms. We show that this system can be simplified to first-order minimal logic with rewrite rules, along the Deduction Modulo Theory lines.

We show that our rewrite system is terminating and that the conversion rule respects weak versions of invertibility of the arrow and of quantifiers. This requires additional care, in particular in the treatment of the latter. Then we study proof reduction, and show that every typable proof term is strongly normalizable and vice-versa.

Automates
vendredi 29 juin 2018, 14h30, Salle 3052
Jacques Sakarovitch (IRIF/CNRS and Telecom ParisTech) The complexity of carry propagation for successor functions

Given any numeration system, we call 'carry propagation' at a number N the number of digits that are changed when going from the representation of N to the one of N+1 , and 'amortized carry propagation' the limit of the mean of the carry propagations at the first N integers, when N tends to infinity, and if it exists.

We address the problem of the existence of the amortized carry propagation and of its value in non-standard numeration systems of various kinds: abstract numeration systems, rational base numeration systems, greedy numeration systems and beta-numeration.

We tackle the problem by means of techniques of three different types: combinatorial, algebraic, and ergodic.

For each kind of numeration systems that we consider, the relevant method allows to establish sufficient conditions for the existence of the carry propagation and examples show that these conditions are close to be necessary.

This is a joint work with Valérie Berthé, Christiane Frougny, and Michel Rigo

Vérification
vendredi 29 juin 2018, 11h00, Salle 3052
Mahsa Shirmohammadi (LIS, CNRS - Univ. Aix-Marseille) Costs and Rewards in Priced Timed Automata

We consider Pareto analysis of reachable states of multi-priced timed automata (MPTA): timed automata equipped with multiple observers that keep track of costs (to be minimised) and rewards (to be maximised) along a computation. Each observer has a constant non-negative derivative which may depend on the location of the MPTA. We study the Pareto Domination Problem, which asks whether it is possible to reach a target location via a run in which the accumulated costs and rewards Pareto dominate a given objective vector. We show that this problem is undecidable in general, but decidable for MPTA with at most three observers. For MPTA whose observers are all costs or all rewards, we show that the Pareto Domination Problem is PSPACE-complete. We also consider an epsilon-approximate Pareto Domination Problem that is decidable without restricting the number and types of observers. We develop connections between MPTA and Diophantine equations. Undecidability of the Pareto Domination Problem is shown by reduction from Hilbert's 10th Problem, while decidability for three observers is shown by a translation to a fragment of arithmetic involving quadratic forms.