Les membres de l'IRIF et les visiteurs sont priés de se conformer aux directives COVID-19 du CNRS et de l'Université de Paris.

Institut de Recherche en Informatique Fondamentale (IRIF)


L'IRIF est une unité mixte de recherche (UMR 8243) entre le CNRS et l'Université de Paris, qui héberge deux équipes-projets Inria.

Les recherches menées à l'IRIF reposent sur l’étude et la compréhension des fondements de toute l’informatique, afin d’apporter des solutions innovantes aux défis actuels et futurs des sciences numériques.

L'IRIF regroupe près de deux cents personnes. Six de ses membres ont été lauréats de l'European Research Council (ERC), cinq sont membres de l'Institut Universitaire de France (IUF) et deux sont membres de l'Academia Europæa.

Université de Paris

Université de Paris has opened one permanent associate professor position in Computer Science. Recruited researcher will join IRIF. Apply by April 9th, 4pm (Paris time).


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.

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.

(Ces actualités sont présentées selon un classement mêlant priorité et aléatoire.)

Tous les évènements sont actuellement organisés à distance (ou suspendus).

Lundi 30 mars 2020, 11 heures, (online, using BigBlueButton)
[Rescheduled] Filip Mazowiecki (MPI SWS) Lower bounds for polynomial recurrence sequences

We study the expressiveness of polynomial recurrence sequences (PRS), a nonlinear extension of the well-known class of linear recurrence sequences (LRS). A typical example of a sequence definable in PRS but not in LRS is a_n = n!. Our main result is that the sequence u_n = n^n cannot be defined by any PRS. We also discuss the impact of our results on the expressiveness of nonlinear extensions of weighted automata. This is joint work with Michaël Cadilhac, Charles Paperman, Michał Pilipczuk and Géraud Sénizergues.

Lundi 30 mars 2020, 11 heures, Salle 1007
[Cancelled] Adrian Francalanza (University of Malta) An Operational Guide to Monitorability

Monitorability underpins the technique of Runtime Verification because it delineates what properties can be verified at runtime. Although many monitorability definitions exist, few are defined explicitly in terms of the operational guarantees provided by monitors, that is the computational entities carrying out the verification. We view monitorability as a spectrum, where the fewer guarantees that are required of monitors, the more properties become monitorable. Accordingly, we present a monitorability hierarchy based on this trade-off. For regular specifications, we give syntactic characterizations in terms of Hennessy–Milner logic with recursion for its levels. Finally, we map existing monitorability definitions into our hierarchy. Hence our work gives a unified framework that makes the operational assumptions and guarantees of each definition explicit. This provides a rigorous foundation that can inform design choices and correctness claims for runtime verification tools.

Algorithmes et complexité
Mardi 31 mars 2020, 14 heures 30, Online
Vincent Jugé (LIGM) Adaptive ShiversSort - A new sorting algorithm

I will present a sorting algorithm called adaptive ShiversSort. This recently developed algorithm improves the speed at which it sorts arrays by using the existence of already sorted subarrays. I will focus on the links between this algorithm and the algorithm TimSort, which is a standard algorithm in Python and Java. I will also show that the complexity of adaptive ShiversSort, in terms of comparisons performed, is optimal up to an additive linear factor.

Live stream: https://bbb2.math.univ-paris-diderot.fr/b/yas-gge-2ka

Séminaire des doctorants
Mercredi 1 avril 2020, 11 heures, Online
Simona Etinski (IRIF & INRIA) Non encore annoncé.

Vendredi 3 avril 2020, 14 heures 30, Online
Nathanaël Fijalkow (LaBRI) Assume Guarantee Synthesis for Prompt Linear Temporal Logic

An assume guarantee (AG) specification is of the form “Assumption implies Guarantee”. AG Synthesis is the following problem: given an AG specification, construct a system satisfying it.

In this talk I will discuss the case where both Assumptions and Guarantees are given by Prompt Linear Temporal Logic (Prompt LTL), which is a logic extending LTL by adding bound requirements such as “every request is answered in bounded time”.

The solution to the AG problem for Prompt LTL will be an invitation to the theory of regular cost functions.

Joint work with Bastien Maubert and Moshe Y. Vardi.

Séminaire Virtuel sur BigBlueButton

Lundi 6 avril 2020, 11 heures, (online, using BigBlueButton)
Amaury Pouly (CNRS & IRIF) Non encore annoncé.