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

## Actualités

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

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

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

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

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

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

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

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

*08.12.2017*

Ludovic Patey was awarded the Prix Thiessé de Rosemont / Demassieux for his PhD thesis « Les mathématiques à rebours de théorèmes de type Ramsey », supervised by Laurent Bienvenu and Hugo Herbelin.

## Événements

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) *Species of structure: a Bridge between Differential Lambda Calculus and Combinatorics & Verifying Database Histories*

*Species of structure: a Bridge between Differential Lambda Calculus and Combinatorics*

Species of structure lie at the intersection of combinatorics and denotational semantics. They were first introduced by Joyal as a unified framework for the theory of generating series in enumerative combinatorics and multiple tools were developed for the resolution of differential equations of species in this setting. Later, Fiore presented a generalized definition that both encompasses Joyal's species and constitutes a model of linear logic.

We will first introduce and connect the different viewpoints of species of structure and their series counterpart (analytic and normal functors) presented by Joyal, Girard and Hasegawa. Next, we will examine how the bicategory of generalized species of structure forms a model of differential linear logic.

As our end goal is to develop methods of resolution of differential equations for λ-terms, we will investigate the possible directions to tackle this problem.

&

*Verifying Database Histories*

Popular databases offer control over the isolation level to which the operations in one transaction are visible to the operations in other concurrent transactions. Lower levels allow weaker consistency. So, we have to ensure that the histories of a database are consistent with their isolation levels.

Unfortunately, these isolation levels are mostly defined as low-level operations which makes it complicated to reason about the behavior of the system running under those isolations.

In this talk, we will present some popular isolation levels and consistency criteria for databases. We will introduce a framework, in which it becomes easier to formally reason about the behavior of a system. Then we will explore the complexities of deciding some consistency criteria using that framework.

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

Vérification

lundi 26 février 2018, 11h00, Salle 1007

**Cătălin Hriţcu** (INRIA) *tba*

tba