Institut de Recherche en Informatique Fondamentale (IRIF)


Université Paris Cité

L'IRIF est une unité mixte de recherche (UMR 8243) entre le CNRS et l'Université Paris Cité, 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), trois 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.


Congratulations to Jean Krivine (IRIF) and Vincent Danos (ENS and CNRS) who have received the Concur Test-of-Time Award (period 2002-2005) for their article “Reversible Communicating Systems”, published at CONCUR 2004. To read their article :

Juliette Calvi, la nouvelle assistante de communication de l'IRIF est arrivée depuis la semaine dernière. N'hésitez pas à lui faire part de tous vos besoins en communication ou simplement à aller la rencontrer dans son bureau 4004.

François Métayer

À l’occasion du départ à la retraite de François Métayer, le LHC rendra hommage au spécialiste des polygraphes, de l’homotopie et de la réécriture, animateur d’un groupe de travail mythique sur ces sujets. L’événement aura lieu les *8 et 9 juin 2023 et sera précédé par les journées LHC

Claire Mathieu

Claire Mathieu a été citée dans un article du journal “La Croix” : “Intelligence artificielle : “pourquoi sa vision du monde est-elle si biaisée ?

Journées PPS 2023

Le pôle PPS organise ses journées 2023, les 25 et 26 mai prochains, et c'est ouvert à tous.


The ANR CoREACT will have its kick-off on Wednesday 19 April. It will be in room 146 and online, open to everyone. Contact Nicolas Behr for the details.

Claire Mathieu

We are proud to announce that Claire Mathieu was named as recipient of an EATCS fellowship for her fundamental contributions to solving theoretical and applied problems in approximation algorithms, online algorithms, and auction theory.

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

Combinatoire énumérative et analytique
Jeudi 1 juin 2023, 11 heures, IHP
Seminaire Flajolet Julien Courtiel, Anna Ben-Hamou, Christophe Hohlweg

Séminaire des membres non-permanents
Jeudi 1 juin 2023, 16 heures, Olympe de Gouges 147 and Zoom link
Thomas Colcombet Non encore annoncé.

La syntaxe rencontre la sémantique
Jeudi 1 juin 2023, 14 heures, salle 146 (Olympe de Gouges)
Gabriele Vanoni (Univ. Bologna) Higher-Order and Non-Linear Bayesian Networks

Catégories supérieures, polygraphes et homotopie
Vendredi 2 juin 2023, 14 heures, Olympe de Gouges
Noam Zeilberger (LIX) Parsing as a lifting problem and the Chomsky-Schützenberger representation theorem

The classical statement of the Chomsky-Schützenberger representation theorem says that any context-free language may be represented as the homomorphic image of the intersection of a Dyck language of balanced parentheses with a regular language. In the talk I will discuss a fibrational perspective on context-free grammars and finite-state automata that grew out of a long-running project with Paul-André Melliès on type refinement systems, but with a surprising twist that only emerged when we considered the C-S theorem. It turns out that underlying that theorem is a basic adjunction between categories and colored operads (= multicategories), where the right adjoint $W : Cat \to Oper$ builds a “spliced arrow operad” out of any category, and the left adjoint $C : Oper \to \Cat$ sends any operad to a “contour category” whose arrows have a geometric interpretation as oriented contours of operations.

Based on joint work with Paul-André Melliès that appeared at MFPS 2022 (, as well as a long version of that article in preparation.

Vendredi 2 juin 2023, 14 heures, Salle 146 Olympe de Gouges
Alexandra Rogova ([DB]) GPC: A Pattern Calculus for Property Graphs

Joint work with Nadime Francis, Amélie Gheerbrant, Paolo Guagliardo, Leonid Libkin, Victor Marsault, Wim Martens, Filip Murlak, Liat Peterfreund and Domagoj Vrgoč The development of practical query languages for graph databases runs well ahead of the underlying theory. The ISO committee in charge of database query languages is currently developing a new standard called Graph Query Language (GQL), the main component of which is the pattern matching facility. In many aspects, it goes well beyond RPQs, CRPQs, and similar queries on which the research community has focused for years. In this talk, I will present our distillation of the lengthy standard into a simple Graph Pattern Calculus (GPC) that reflects all the key pattern matching features of GQL.

Graph Transformation Theory and Applications
Vendredi 2 juin 2023, 15 heures, online
Fernando Orejas (Department of Computer Science, Universitat Politècnica de Catalunya, Spain) Unification of Drags and Confluence of Drag Rewriting

Drags are a recent, natural generalization of terms which admit arbitrary cycles. A key aspect of drags is that they can be equipped with a composition operator so that rewriting amounts to replace a drag by another in a composition. In this paper, we develop a unification algorithm for drags that allows to check the local confluence property of a set of drag rewrite rules.

Zoom meeting registration link

YouTube live stream

Lundi 5 juin 2023, 11 heures, Olympe de Gouges 146 and Zoom link
Pedro Ribeiro (University of York) Co-verification for robotics: simulation and verification by proof

Robots are facilitating new business models from food delivery to healthcare. Current engineering practice cannot yet provide the formal guarantees needed to allay the safety concerns of regulators. Simulation, a technique favoured by practitioners, provides an avenue for experimenting with different scenarios before committing to expensive tests and proofs. In this talk, I will discuss how different models may be brought together for the (co-)verification of system properties, with simulation complementing formal verification. This will be explored in the context of the model-driven RoboStar framework, that clearly identifies models of the software, hardware, and scenario, and has heterogeneous formal semantics amenable to verification using model-checkers and theorem provers.

Algorithmes et complexité
Mardi 6 juin 2023, 11 heures, Salle 147 (Olympe de Gouges)
Galina Pass (QuSoft, University of Amsterdam) (No) Quantum space-time tradeoff for USTCON

Analyse et conception de systèmes
Mercredi 7 juin 2023, 14 heures, Salle 146 (Olympe de Gouges)
Samuel Vivien (ENS Paris, IRIF) How to prove that you need Cake ?

PureCake, is a mechanically-verified compiler for PureLang, a lazy, purely functional programming language with monadic effects. PureLang syntax is Haskell-like and indentation-sensitive, and its constraint-based Hindley-Milner type system guarantees safe execution. This talk will present how optimization soundness can be proven using equational reasoning with the example of the demand analysis pass and other related optimizations.

Based on : PureCake: A Verified Compiler for a Lazy Functional Language [PLDI'23] by Hrutvik Kanabar, Samuel Vivien, Oskar Abrahamsson, Magnus O. Myreen, Michael Norrish, Johannes Åman Pohjola, Riccardo Zanetti

Combinatoire énumérative et analytique
Jeudi 8 juin 2023, 14 heures, Olympe de Gouges
Davig Forge (Orsay) TBD