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 une équipe-projet 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), deux sont membres de l'Academia Europæa, et un est membre de l'Académie des sciences.

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 !

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.

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.

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.

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.

Logic in Computer Science

Ralph Sarkis (IRIF), Matteo Mio (LIP, ENS Lyon) and Valeria Vignudelli (LIP, ENS Lyon) will present at LICS2021 equational and metric reasoning tools for programs combining nondeterminism, probability and termination.

CanaDAM conference 2021

Three papers coauthored by IRIF members will be presented at the CanaDAM conference 2021, May 25-28.

On the logical structure of choice and bar induction principles

Nuria Brede (University of Potsdam) and Hugo Herbelin (IRIF) will present at LICS21 a unified classification of choice and bar induction principles.

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

Lundi 14 juin 2021, 11 heures, 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.

Algorithmes et structures discrètes
Mardi 15 juin 2021, 14 heures, 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
Mardi 15 juin 2021, 14 heures 30, 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.

Théorie des types et réalisabilité
Mercredi 16 juin 2021, 14 heures, online (
Félix Castro (IRIF) Proving Church Thesis in Heyting Arithmetic with Lisp's quote

Preuves, programmes et systèmes
Jeudi 17 juin 2021, 10 heures, 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.

Vendredi 18 juin 2021, 14 heures 30,
Charles Paperman Non encore annoncé.