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 one Inria project-team.

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), two are members of the Academia Europæa, and one is member of Académie des sciences.

Accepted paper LICS'21

Claudia Faggian (IRIF) and Francesco Gavazzo (U. Bologna) will present at LICS21 a foundation for monadic rewriting, and its application to calculi with algebric effects.

Accepted paper LICS'21

Paul-André Melliès (IRIF) will present at LICS 2021 an asynchronous template game semantics where the shuffle tensor product of asynchronous games is formulated for the first time as the Gray tensor product of 2-categories, with appropriate scheduling template.

Entretien quantique - Collège de France

Invité sur la chaire annuelle Informatique et sciences numériques du Collège de France 2020-2021, le Professeur Frédéric Magniez discute de la naissance de l'écosystème de l'informatique quantique. Lisez son interview !

LICS 2021- Accepted paper

Thomas Ehrhard (IRIF) and Farzad Jafarrahmani (Université de Paris) will present at LICS2021 the first categorical semantics of Linear Logic with induction and coinduction.

LICS 2021 - Accepted papers

Antoine Allioux (IRIF), Eric Finster (Cambridge University), and Matthieu Sozeau (Inria) will present at LICS 2021 a proof that types are infinity-groupoids internal to an extension of homotopy type theory allowing for the formalization of higher algebraic structures.

Accepted papers LAGOS'21

Two papers coauthored by IRIF members will be presented at the Latin and American Algorithms, Graphs and Optimization Symposium (LAGOS), May 17-21.

Portrait de Pierre-Evariste Dagand

IRIF has the great pleasure to welcome a new research scientist (CNRS) : Pierre-Evariste Dagand, an expert in language programming. Learn more about him and his work.

Parametricity and Semi-Cubical Types

Hugo Moeneclaey (IRIF) will present at LICS 2021 a construction semi-cubical models of type theory as cofree parametric models.

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

Monday June 14, 2021, 11AM, 3052 and BBB link
Arnaud Sangnier (IRIF, Université de Paris) Reachability in Distributed Memory Automata

We introduce Distributed Memory Automata, a model of register automata suitable to capture some features of distributed algorithms designed for shared memory systems. In this model, each participant owns a local register and a shared register and has the ability to change its local value, to write it in the global memory and to test atomically the number of occurrences of its value in the shared memory, up to some threshold. We show that the control state reachability problem for Distributed Memory Automata is Pspace-complete for a fixed number of participants and is in Pspace when the number of participants is not fixed a priori.

This is a joint work with Benedikt Bollig and Fedor Ryabinin.

Algorithms and discrete structures
Tuesday June 15, 2021, 2PM, Salle 3052
Magnús Halldórsson (Reykjavik University) New Vistas in Distributed Graph Coloring

The first and possibly the most fundamental problem in distributed graph algorithmics is the vertex coloring problem. The nodes of a network are processes that communicate via the edges in synchronous rounds. The most basic problem is to color the network using Delta+1 colors in as few rounds a possible, where Delta is the maximum degree of the graph.

We present a new approach for randomized distributed Delta+1-coloring that is dramatically simpler than the previous best: the seminal work of Chang, Li, and Pettie (CLP) in SICOMP 2020. This approach offers numerous refinements: It matches the O(log^3 log n) round complexity in general, while on high-degree graphs (Delta » log^2 n), it uses only O(log* n) rounds. It uses small messages, i.e., works also in the CONGEST model. It also offers tradeoffs between the number of colors used, the round complexity, and the clique number of the graph.

We expect that the approach presented will lead the way towards improved results for various coloring problems in the near future.

This is based on a paper at STOC'21, joint work with Fabian Kuhn, Yannic Maus, and Tigran Tonoyan; and a more recent one on arXiv, joint with Alexandre Nolin, and Tigran Tonoyan.

One world numeration seminar
Tuesday June 15, 2021, 2:30PM, Online
Sam Chow (University of Warwick) Dyadic approximation in the Cantor set

We investigate the approximation rate of a typical element of the Cantor set by dyadic rationals. This is a manifestation of the times-two-times-three phenomenon, and is joint work with Demi Allen and Han Yu.

Type theory and realisability
Wednesday June 16, 2021, 2PM, online (
Félix Castro (IRIF) Proving Church Thesis in Heyting Arithmetic with Lisp's quote

Proofs, programs and systems
Thursday June 17, 2021, 10AM, Online
Sonia Marin Focused nested calculi applied to the logic of bunched implications

Focusing is a general technique for syntactically compartmentalising the non-deterministic choices in a proof system, which not only improves proof search but also has the representational benefit of distilling sequent proofs into synthetic normal forms. However, since focusing was traditionally specified as a restriction of the sequent calculus, the technique had not been transferred to logics that lack a (shallow) sequent presentation, as is the case for some modal or substructural logics.

With K. Chaudhuri and L. Straßburger, we extended the focusing technique to nested sequents, a generalisation of ordinary sequents which allows us to capture all the logics of the classical and intuitionistic S5 cube in a modular fashion. This relied, following the method introduced by O. Laurent, on an adequate polarisation of the syntax and an internal cut-elimination procedure for the focused system which in turn is used to show its completeness.

Recently, with A. Gheorghiu, we applied a similar method to the logic of Bunched Implications (BI), a logic that freely combines intuitionistic logic and multiplicative linear logic. For this we had first to reformulate the traditional bunched calculus for BI using nested sequents, followed by a polarised and focused variant that (again) we show is sound and complete via a cut-elimination argument.

Friday June 18, 2021, 2:30PM,
Charles Paperman To be announced.