Institut de Recherche en Informatique Fondamentale(IRIF)


IRIF, the Research Institute on the Foundations of Computer Science, is a research laboratory of CNRS and Université de Paris, also hosting two Inria project-teams.

The research conducted at IRIF is based on the study and understanding of the foundations of all computer science, in order to provide innovative solutions to the current and future challenges of digital sciences.

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

The ANR PPS kick-off meeting will take place from Feb 26 to Feb 28, 2020 at IRIF (Paris) and will be joined with the 3rd edition of the PIHOC workshop series initiated by Ugo Dal Lago in 2018 and with Dal Lago's DIAPASoN ERC project kick-off meeting. Register by Jan 31: registration is free but mandatory.

IRIF will finance one or two additional Master scholarships in Foundations of Computer Science within the PGSM program of FSMP for female students who have completed a bachelor’s degree or the first year masters in one of the universities of the FSMP network. Apply by May 8th.

JFLA 2020

Yann Régis-Gianas (IRIF) is the vice-president of the “Journées Francophones des Langages Applicatifs” that will take place at Gruissan from the 29th of January to the 1st of February.


Sylvain Périfel from IRIF, together with Damiano Mazza and Thomas Seiller, organize the Caleidoscope Research School in Computational Complexity, to be held in Paris, 15-19 June 2020.

(These news are displayed using a randomized-priority ranking.)

Monday February 24, 2020, 11AM, Salle 1007
James Worrell (University of Oxford) Termination of linear constraint loops

We consider the problem of deciding termination of linear constraint loops, that is, single-path loops in which the loop body consists of a (possibly non-deterministic) assignment, specified a conjunction of linear constraints. We present several versions of this problem, according to the syntactic form of the loop and the numerical domain of the program variables. We sketch some decidability results and point out open problems.

Tuesday February 25, 2020, 2PM, Salle 3052
Georg Zetsche (MPI SWS) Extensions of $\omega$-Regular Languages

We consider extensions of monadic second order logic over $\omega$-words, which are obtained by adding one language that is not $\omega$-regular. We show that if the added language $L$ has a neutral letter, then the resulting logic is necessarily undecidable. A corollary is that the $\omega$-regular languages are the only decidable Boolean-closed full trio over $\omega$-words.

(Joint work with Mikołaj Bojańczyk, Edon Kelmendi, and Rafał Stefański)

Note the unusual time (14:00).

Enumerative and analytic combinatorics
Thursday February 27, 2020, 2PM, Salle 1007
Sandro Franceschi (Université Paris-sud) Invariants de Tutte et Brownien réfléchi dans un cône

Dans les années 1970, William Tutte développa une approche algébrique, basée sur des « invariants », pour résoudre une équation fonctionnelle qui apparait dans le dénombrement de triangulations colorées. La transformée de Laplace de la distribution stationnaire du mouvement brownien réfléchi dans des cônes satisfait une équation similaire. Pour être applicable, cette méthode requiert l’existence de deux fonctions appelées respectivement invariant et fonction de découplage. Tous les modèles ont des invariants mais on démontre que l’existence de fonctions de découplage équivaut à une condition géométrique simple sur les angles de réflexion. Pour les modèles qui ont une fonction de découplage, on obtient une expression explicite sans intégrale de la transformée de Laplace en fonction des invariants. En particulier, on obtient à nouveau une formule pour la transformée de Laplace de plusieurs cas bien connus, comme la skew symétrie, les réflexions orthogonales ou le résultat de Dieker et Moriarty qui caractérise les densités stationnaires qui s’écrivent sous la forme d’une somme d’exponentielles. Cette méthode permet de plus de caractériser la nature algébrique de la transformée de Laplace en fonction des modèles. Cet exposé est issu d’un travail en collaboration avec M. Bousquet-Mélou, A. Elvey Price, C. Hardouin et K. Raschel.

Higher categories, polygraphs and homotopy
Thursday February 27, 2020, 2PM, Salle 1012
Michael Batanin (IHES) Comparing symmetric operads and operadic categories

The notion of operadic category appeared in the work of Batanin and Markl as a tool for working with various operad like structures. Each operadic category O has an associated category of O-operads with values in an arbitrary symmetric monoidal category. Operadic categories and operadic functors form a category.

In my talk I will show that the category of symmetric operads in Set (variation of colours is allowed) is a reflective subcategory of the category of operadic categories. The inclusion is given by (operadic) Grothendieck construction and the reflection is given by evaluation of the left Kan extension along arity functor on the terminal operad. Thus the notion of operadic category can be considered as a flexible extension of the notion of symmetric operad.

Moreover, there is yet another functor from operadic categories to symmetric operads which sends an operadic category O to a symmetric operad in Set whose algebras are exactly O-operads. These three functors (Grothendieck construction, its left adjoint and free operad functor) fit in a nice picture with a universal property. In particular, they various composites generate the Baez-Dolan +-constructions for both symmetric operads and operadic categories.

*Attention : date et salle inhabituelles !*

Higher categories, polygraphs and homotopy
Friday February 28, 2020, 2PM, Salle 1007
Sebastian Posur (Universität Siegen) Methods of constructive category theory

Categorical abstraction is a powerful organizing principle in computer algebra. In this talk, we explain the concept of constructive category theory and how we implement this concept in our software project CAP-Categories, algorithms, programming. In CAP it is possible to implement higher algorithms and data structures using basic categorical operations as primitives, which in turn often rely on classical algorithms in computer algebra like the computation of Gröbner bases. As an example, we show how our categorical framework can be used for computing with finitely presented functors.

Friday February 28, 2020, 2:30PM, Salle 3052
Marie Van Den Bogaard (ULB) Subgame Perfect Equilibria in Quantitative Reachability Games

In this talk, we consider multiplayer games on graphs. In such games, each player has his own objective, that does not necessarily clash with the objectives of the other players. In this “non zero-sum” context, equilibria are a better suited solution concept than the classical winning strategy notion. We will focus on a refinement of the well-known Nash Equilibrium concept: Subgame Perfect Equilibrium (SPE for short), where players have to play rationnally in every scenario, even the ones that deviate from the planned outcome. We will explain why this refinement is a relevant solution concept in multiplayer games and show how to handle them in quantitative reachability games, where each player wants to minimize the number of steps to reach its own target set of vertices.