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 deux sont membres de l'Institut Universitaire de France (IUF).


Paris Diderot

05.02.2017
Université Paris Diderot has opened three permanent positions in Computer Science (1 professor on Graph and applications, 1 assistant professor on Software Science, 1 assistant professor on Data Science). Recruited researchers will join IRIF.

Amina Doumane

04.02.2017
Laurent Viennot (IRIF, Inria) is Scientific Curator of the exhibition Informatique et sciences du numérique, at Palais de la découverte, starting March 13, 2018.

Amina Doumane

02.02.2017
Amina Doumane Amina Doumane now at LIP was awarded the prize “La Recherche” in the Computer Science category for her paper entitled Constructive Completeness for the linear-time mu-calculus, a work accomplished during her PhD at IRIF and that appeared in the proceedings of LICS’17.

Nature

01.02.2017
The first on-the-fly quantum money transaction was implemented by researchers in Paris, including Iordanis Kerenidis. ​Quantum ​money is provably unforgeable​ due to the no-cloning property of quantum information.​

LIA INFINIS

27.01.2017
The international French and Argentina CNRS laboratory called INFINIS lead by Delia Kesner (IRIF) and Sergio Yovine (CONICET) is presented in the CNRS Rio newsletter.

Maurice Nivat

18.01.2018
IRIF organizes on February the 6th a Scientific Day in memory of Maurice Nivat, professor at Paris Diderot University and a pionneer of theoretical computer science. Please register.

ITCS

05.01.2018
Lucas Boczkowski and Amos Korman from IRIF, with their co-authors, will present at ITCS 2018 a non-conditional lower bound on information dissemination in stochastic populations. The paper is the first ever to combine an algorithmic lower bound with a biology experiment in collective behavior.

CIFRE

19.12.2017
IRIF and ATOS have started the first Industrial PhD Thesis (CIFRE) on quantum algorithms in France. The PhD candidate Alessandro Luongo is co-advised by Iordanis Kerenidis and Frédéric Magniez.

Analyse et conception de systèmes
lundi 19 février 2018, 11h00, Salle 3052
Adrien Boiret (University of Warsaw) The “Hilbert Method” for Solving Transducer Equivalence Problems

Classical results from algebra, such as Hilbert's Basis Theorem and Hilbert’s Nullstellensatz, have been used to decide equivalence for some classes of transducers, such as HDT0L (Honkala 2000) or more recently deterministic tree-to-string transducers (Seidl, Maneth, Kemper 2015). In this talk, we propose an abstraction of these methods. The goal is to investigate the scope of the “Hilbert method” for transducer equivalence that was described above.

Consider an algebra A in the sense of universal algebra, i.e. a set equipped with some operations. A grammar over A is like a context-free grammar, except that it generates a subset of the algebra A, and the rules use operations from the algebra A. The classical context-free grammars are the special case when the algebra A is the free monoid with concatenation. Using the “Hilbert method” one can decide certain properties of grammars over algebras that are fields or rings of polynomials over a field. The “Hilbert method” extends to grammars over certain well-behaved algebras that can be “coded” into fields or rings of polynomials. Finally, for these well-behaved algebras, one can also use the “Hilbert method” to decide the equivalence problem for transducers (of a certain transducer model that uses registers) that input trees and output elements of the well-behaved algebra.

In the talk, we give examples and non-examples of well-behaved algebras, and discuss the decidability / undecidability results connected to them. In particular:

-We show that equivalence is decidable for transducers that input (possibly ordered) trees and output unranked unordered trees.

-We show that equivalence is undecidable for transducers that input words and output polynomials over the rational numbers with one variable (but are allowed to use composition of polynomials).

Joint work with Mikołaj Bojańczyk, Janusz Schmude, Radosław Piórkowski at Warsaw University.

Vérification
lundi 19 février 2018, 11h00, Salle 3052
Adrien Boiret (University of Warsaw) The “Hilbert Method” for Solving Transducer Equivalence Problems.

Classical results from algebra, such as Hilbert's Basis Theorem and Hilbert’s Nullstellensatz, have been used to decide equivalence for some classes of transducers, such as HDT0L (Honkala 2000) or more recently deterministic tree-to-string transducers (Seidl, Maneth, Kemper 2015). In this talk, we propose an abstraction of these methods. The goal is to investigate the scope of the “Hilbert method” for transducer equivalence that was described above.

Consider an algebra A in the sense of universal algebra, i.e. a set equipped with some operations. A grammar over A is like a context-free grammar, except that it generates a subset of the algebra A, and the rules use operations from the algebra A. The classical context-free grammars are the special case when the algebra A is the free monoid with concatenation. Using the “Hilbert method” one can decide certain properties of grammars over algebras that are fields or rings of polynomials over a field. The “Hilbert method” extends to grammars over certain well-behaved algebras that can be “coded” into fields or rings of polynomials. Finally, for these well-behaved algebras, one can also use the “Hilbert method” to decide the equivalence problem for transducers (of a certain transducer model that uses registers) that input trees and output elements of the well-behaved algebra.

In the talk, we give examples and non-examples of well-behaved algebras, and discuss the decidability / undecidability results connected to them. In particular:

-We show that equivalence is decidable for transducers that input (possibly ordered) trees and output unranked unordered trees.

-We show that equivalence is undecidable for transducers that input words and output polynomials over the rational numbers with one variable (but are allowed to use composition of polynomials).

Joint work with Mikołaj Bojańczyk, Janusz Schmude, Radosław Piórkowski at Warsaw University.

Graphes
mardi 20 février 2018, 14h00, Salle 1007
Jan Arne Telle (University of Bergen) Width parameters of graphs and structured graph classes

Tree-width and clique-width are well-known graph parameters of algorithmic use. Clique-width is a stronger parameter in the sense that it is bounded on more classes of graphs. In this talk we will present an even stronger graph parameter called mim-width (maximum induced matching-width). Several nicely structured graphs, like interval graphs, permutation graphs and leaf power graphs, have mim-width 1. Given a decomposition of bounded mim-width of a graph G we can solve many interesting problems on G in polynomial time. We will mention also a yet stronger parameter, sim-width (special induced matching-width), of value 1 even for chordal and co-comparability graphs.

Parts of the talk are based on joint work with O.Kwon and L.Jaffke, to appear at STACS 2018.

Sémantique
mardi 20 février 2018, 11h00, Salle 3052
Shin-Ya Katsumata (National Institute of Informatics, Tokyo) Codensity liftings of monads

I will introduce a method to lift monads on the base category of a fibration to its total category using codensity monads. This method, called codensity lifting, is applicable to various fibrations which were not supported by the speaker's previous method called categorical TT-lifting. After introducing the codensity lifting, we illustrate some examples of codensity liftings of monads along the fibrations from the category of preorders, topological spaces and extended psuedometric spaces. I will also talk about the liftings of algebraic operations to the codensity-lifted monads. If time permits, I will mention a characterisation of the class of liftings (along posetal fibrations with fibred small limits) as a limit of a certain large diagram.

(Joint work with Tetsuya Sato; presented in CALCO 2015)

Exposés hors-séries
mardi 20 février 2018, 14h00, 3052
Daniela Petrisan (IRIF) Up-To Techniques for Behavioural Metrics via Fibrations

Up-to techniques are a well-known method for accelerating proofs of

behavioural equivalences between systems. In this talk, I 
introduce up-to techniques for behavioural metrics in a coalgebraic
setting and provide general results that show under which conditions
such up-to techniques are sound.
For a system modelled as a coalgebra for a certain functor, the
behavioural distance can be seen as a coinductive predicate using a
suitable lifting of the functor. I will focus on the so called
Wasserstein lifting of a functor for which we provide a new
characterization in a fibrational setting. This is useful for
automatically proving the soundness of up-to techniques via a
generic framework developed in a previous CSL-LICS'14 paper.
I will use  fibrations of predicates and relations valued in a
quantale, for which pseudo-metric spaces are an example. To
illustrate our framework I provide an example on distances between
regular languages.

Séminaire des doctorants
mercredi 21 février 2018, 11h00, Salle 3052
Zeinab Galal & Ranadeep Biswas (Algebra and computation & Modeling and verification) TBA

TBA

Preuves, programmes et systèmes
jeudi 22 février 2018, 10h30, Salle 3052
Pierre-Marie Pédrot (Max Planck Institute for Software Systems, Saarbrücken, Germany) Failure is Not an Option, or The Curry-Howard-Shadok correspondence

No one is without knowing the famous Shadok principle « the more it fails, the more likely it will eventually succeed. » Taking inspiration from this unfathomable wisdom, we came up with a dependent type theory which allows failure, so that we could succeed more in proving things. Such a Shadok theory is justified by translating it away into vanilla dependent theory, just as a mundane compiler would, where failing can be interpreted as a call-by-name exception mechanism. En passant, this gives the first full syntactical model of the Calculus of Inductive Constructions introducing effects.

Alas! The right to fail succeeds a tad too much, insofar as the resulting Shadock type theory is logically inconsistent. Not being impressed in any way, we put order into this madness by requiring that no exception should ever reach toplevel, thanks to a clever use of a variant of Bernardy-Lasson syntactic parametricity. While the former model can be thought of as Friedman A-translation applied to CIC, the latter is no more than a principled variant of Kreisel's modified realizability that scales to dependent types. In particular, it readily gives a model of CIC that still has canonicity, strong normalization and decidable type-checking, while featuring new principles typical of modified realizability such as the independence of premises and unprovability of Markov's principle.

https://www.pédrot.fr/articles/exceptional.pdf

Combinatoire énumérative et analytique
jeudi 22 février 2018, 11h45, Salle 1007
Justine Falque (LRI, université Paris-sud 11) Algèbre des orbites des groupes à profil polynomial, théorèmes de Cameron et de Macpherson

Étant donné un groupe de permutation infini G, on définit la fonction qui à tout entier naturel n associe le nombre d'orbites de sous-ensembles de cardinal n, pour l'action induite de G sur les sous-ensembles d'éléments. Cameron a conjecturé que cette fonction de comptage (le profil de G) est un quasi-polynôme dans le cas où sa croissance est polynomiale. Une autre conjecture, plus forte, a été émise plus tard par un de ses étudiants, Macpherson. Elle concerne une certaine structure d'algèbre graduée sur les orbites de sous-ensembles, créée par Cameron, et suppose que si le profil de G est polynomial, alors son algèbre des orbites est de type fini. L'exposé présentera ces deux conjectures et leur contexte, ainsi que les idées de la preuve de la conjecture de Macpherson, fruit d'un travail commun de Nicolas Thiéry et Justine Falque (avec les conseils précieux de Peter Cameron lui-même).