IRIF is a research laboratory of CNRS and Université Paris-Diderot, also hosting two INRIA project-teams.

The scientific objectives of IRIF are at the core of computer science and, in particular, they focus on the conception, analysis, proof, and verification of algorithms, programs, and programming languages. They are built upon fundamental research activities developed at IRIF on combinatorics, graphs, logics, automata, type, semantics, and algebras.

IRIF hosts about 200 people. Six of its members have been distinguished by the European Research Council (ERC), and two of them are members of the Institut Universitaire de France (IUF).

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.

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 Paris) When Good Components Go Bad: Formally Secure Compilation Despite Dynamic Compromise

We propose a new formal criterion for secure compilation, giving strong end-to-end security guarantees for software components written in unsafe, low-level languages with C-style undefined behavior. Our criterion is the first to model _dynamic_ compromise in a system of mutually distrustful components running with least privilege. Each component is protected from all the others—in particular, from components that have encountered undefined behavior and become compromised. Each component receives secure compilation guarantees up to the point when it becomes compromised, after which an attacker can take complete control over the component and use any of its privileges to attack the remaining uncompromised components. More precisely, we ensure that dynamically compromised components cannot break the safety properties of the system at the target level any more than equally privileged components without undefined behavior already could in the source language.

To illustrate this model, we build a secure compilation chain for an unsafe language with buffers, procedures, and components. We compile it to a simple RISC abstract machine with built-in compartmentalization and provide thorough proofs, many of them machine-checked in Coq, showing that the compiler satisfies our secure compilation criterion. Finally, we show that the protection guarantees offered by the compartmentalized abstract machine can be achieved at the machine-code level using either software fault isolation or a tag-based reference monitor.

Combinatoire énumérative et analytique
mardi 27 février 2018, 14h00, À confirmer
Dieter Mitsche (Université de Nice Sophia-Antipolis) TBA