Institut de Recherche en Informatique Fondamentale

IRIF Université Paris 7 CNRS L'IRIF est une unité mixe de recherche (UMR 8243) du CNRS et de l'Université Paris-Diderot, issue de la fusion des deux UMR LIAFA et PPS au 1er janvier 2016.

Ses objectifs scientifiques se déclinent selon trois grandes thématiques au cœur de l'informatique : les fondements mathématiques de l’informatique ; les modèles de calcul et de preuves ; la modélisation, les algorithmes et la conception de systèmes.

Poste de maître de conférences

Un poste de maître de conférences est ouvert au concours 2017, affecté à l'IRIF, sur les thématiques de l'unité. Consulter la fiche de poste.

Prochains séminaires

Jeudi 23 mars 2017 · 10h30 · Salle 3052

Preuves, programmes et systèmes · Thomas Leventis (Institut de Mathématiques de Marseille) · Full Abstraction of the Probabilistic Böhm Trees

A very natural notion of equivalence of programs is the observational equivalence: two programs are equivalent if they have the same behaviour in any environment. More specifically in the lambda-calculus two terms M and N are equivalent if for every context C, the terms C[M] and C[N] are either both solvable or both unsolvable. Respecting this equivalence is an important property of some models of the lambda-calculus, called the full abstraction. It is well known that the model of infinitely extensional Böhm trees is fully abstract. The question we are interested in is what becomes of these notions when we introduce probabilistic choice in the calculus.

The solvability has a natural extension, which is the convergence probability, hence two terms are observationally equivalent if they have the same convergence probability under any context. There is also a simple way to define probabilistic Bohm trees, as we can associate to any term a subprobability distribution over head normal forms. But it is not obvious that these generalizations of the deterministic notions are still equivalent. In this talk we will show how to prove that probabilistic Böhm trees actually form a model, and how to get a separability result to ensure this model is fully abstract.

Vendredi 24 mars 2017 · 14h30 · Salle 1006

Automates · Martin Delacourt (U. Orléans) · Des automates cellulaires unidirectionnels permutifs et du problème de la finitude pour les groupes d'automates.

On s'intéresse au parallèle entre 2 problèmes sur des modèles distincts d'automates. D'une part, les automates de Mealy (transducteurs lettre à lettre complets) qui produisent des semi-groupes engendrés par les transformations sur les mots infinis associées aux états. En 2013, Gillibert a montré que le problème de la finitude de ces semi-groupes était indécidable, en revanche la question est ouverte dans le cas où l'automate de Mealy produit un groupe. D'autre part, les automates cellulaires unidirectionnels pour lesquels la question de la décidabilité de la périodicité est ouverte. On peut montrer l'équivalence de ces problèmes. On fera un pas vers une preuve d'indécidabilité en montrant qu'il est possible de simuler du calcul Turing dans un automate cellulaire unidirectionnel réversible, rendant ainsi des problèmes de prédiction indécidables ainsi que la question de la périodicité partant d'une configuration donnée finie.

Lundi 27 mars 2017 · 11h00 · Salle 1007

Vérification · Mohamed Faouzi Atig (Uppsala University) · Lossy Channel Systems with Data.

Lossy channel systems are a classical model with applications ranging from the modelling of communication protocols to programs running on weak memory models. All existing work assume that messages traveling inside the channels are picked from a finite alphabet. In this talk, we present two extensions of lossy channel systems. In the first part of the talk, we extend lossy channel systems by assuming that each message is equipped with a clock representing the age of the message, thus obtaining the model of Timed Lossy Channel Systems (TLCS). We show that the state reachability problem is decidable for TLCS.

In the second part of the talk, we extend lossy channel systems by considering systems that operate on a finite set of variables ranging over an infinite data domain. Furthermore, each message inside a channel is equipped with a data item representing its value. Although we restrict the model by allowing the variables to be only tested for (dis-)equality, we show that the state reachability problem is undecidable. In light of this negative result, we consider bounded-phase reachability, where the processes are restricted to performing either send or receive operations during each phase. We show decidability of state reachability in this case by computing a symbolic encoding of the set of system configurations that are reachable from a given configuration.

This talk is based on previous joint work with Parosh Aziz Abdula, Jonathan Cederberg and C. Aiswarya.

Mardi 28 mars 2017 · 14h00 · Salle 1007

Algorithmique distribuée et graphes · Juho Hirvonen (IRIF) · Recent developments in the theory of distributed graph algorithms

I will survey and try to explain the intuition behind several recent developments in the theory of distributed graph algorithms. I will focus on the LOCAL model, where the measure of interest is how far information has to be propagated in a communication network in order solve a given problem. The problems of interest will be locally checkable labelling problems (LCLs), a natural class of problems that allow distributed verification of proposed solutions.

I will discuss two recent papers in this field. First, we gave a lower bound showing that there exist LCL problems of ”intermediate” complexity, that is, complexity strictly between known complexity classes (Brandt et al., STOC 2016). The proof is by a new kind of simulation argument. Second, Chang et al. (FOCS 2016) showed that this lower bound implies an exponential separation between the randomized and deterministic LOCAL models. Chang et al. also show further connections between the randomized and deterministic models, and establish a useful speed-up simulation for the deterministic LOCAL model.

Jeudi 30 mars 2017 · 10h30 · Salle 3052

Preuves, programmes et systèmes · Giovanni Bernardi (IRIF) · Un, personne et cent mille: a meta theory for testing equivalences?

Testing theory focuses on contextual equivalences that were proposed in the 80s as an alternative to bisimulation equivalence. During the last decade testing equivalences proved useful in constructing semantic models of session types and in laying the foundations of web-service technologies. As result, testing theory is more useful and richer than ever. In this seminar I will recall the chief ideas behind testing theory, and argue that we lack a general methodology to reason on testing equivalences. I will also outline the evidence that a meta-theory may exist, and some open questions.