IRIF members and visitors are asked to comply with the COVID-19 Directives of CNRS and Université de Paris.

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.

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.

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

All events are currently organized remotely (or postponed).

Monday March 30, 2020, 11AM, (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.

Monday March 30, 2020, 11AM, 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.

Algorithms and complexity
Tuesday March 31, 2020, 2:30PM, 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:

PhD students seminar
Wednesday April 1, 2020, 11AM, Online
Simona Etinski (IRIF & INRIA) To be announced.

Friday April 3, 2020, 2:30PM, 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

Monday April 6, 2020, 11AM, (online, using BigBlueButton)
Amaury Pouly (CNRS & IRIF) To be announced.