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.

Giuseppe Castagna (IRIF), Mickaël Laurent (Université de Paris), Kim Nguyen (Université Paris Saclay) and Matthew Lutze (Université de Paris) will present their paper that shows a nifty way to use classic deduction rules to define a formal framework in which dynamic languages such as JavaScript can statically and precisely typed. Check the proof-of-concept implementation available at

Accepted papers POPL 2022

Three accepted papers coauthored by IRIF members will be presented at POPL 2022, the main conference on programming languages and programming systems, January 16-22.

Portrait Matej Stehlik

IRIF has the great pleasure to welcome a new professor in computer science at Université de Paris: Matěj Stehlík, an expert in graph theory. Learn more about him and his work here.


IRIF is very pleased to host for one month Serge Massar, Professor at the Université libre de Bruxelles (ULB) as part of the FSMP Distinguished Professor Fellowship. Serge Massar is the director of the Laboratoire d'Information Quantique (LIQ), of the Physics Department, Science Faculty, ULB. His research interests are quantum information theory, experimental quantum and non linear optics, machine learning.

Accepted paper FOCS 2021

Adrian Vladu's paper Faster Sparse Minimum Cost Flow by Electrical Flow Localization, jointly written with Kyriakos Axiotis and Aleksander Madry, will be presented at FOCS 2021.

hpcqs project

We are excited to be part of the “High-Performance Computer and Quantum Simulator hybrid” (HPCQS) aiming at creating a world-class supercomputing ecosystem. Learn more about the project here.


Prochaine conférence dans le cadre des 75 ans d’informatique : L’informatique dans le 7ème art : fiction ou réalité ? Rendez-vous avec Fabrice Kordon le jeudi 9 décembre-18h00 sur le campus Pierre et Marie Curie de Sorbonne Université (tour 25.26, 1er étage – salle 105).

Journée pôle ASV 2021

The Automata, Structures, and Verification (ASV) day is scheduled this year on Friday November 19th. This will be the opportunity to meet again and learn about some of the work done in our pole, in particular by the new comers. Schedule and details of the talks here.

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

Lundi 6 décembre 2021, 11 heures, 1007 and Zoom link
Alessio Mansutti (University of Oxford) Efficient complementation of semilinear sets and the VC dimension of Presburger arithmetic

We discuss the issue of deciding the first-order theory of integer linear arithmetic, also known as Presburger arithmetic. Whereas optimal decision procedures based on either quantifier-elimination or automata constructions are known for this theory, the current procedures based on manipulating semilinear sets (i.e. sets that geometrically characterise the solutions of a formula) are extremely inefficient. We address this issue by deriving a new algorithm for computing the complement of a semilinear set, which in particular is optimal for nested complementations. Alongside solving the aforementioned discrepancy between semilinear-based algorithms and other types of procedures, this result allows us to characterise the Vapnik-Chervonenkis dimension of Presburger arithmetic, which is found to be doubly-exponential. The results in this talk are joint work with Christoph Haase and Dmitry Chistikov.

Algorithmes et complexité
Mardi 7 décembre 2021, 11 heures, Salle 1007
Bruce Kapron (Computer Science Department, University of Victoria) Type-two feasibility via bounded query revision

The problem of generalizing the notion of polynomial time to a type-two setting, where inputs include not only finitary data, e.g., numbers or strings of symbols, but also functions on such data, was first posed by Constable in 1973. Mehlhorn subsequently proposed a solution, based on a generalization Cobham's scheme-based approach which uses limited recursion on notation. The resulting class was shown to be robust with respect to oracle Turing machine (OTM) computation, but the problem of providing a purely machine-based characterization remained open for almost two decades, when Kapron and Cook gave a solution using notions of function length and second-order polynomials. While a natural generalization of the usual notion of poly-time, this characterization still had some shortcomings, as function length is itself not a feasible notion. A charaterization using ordinary polynomials remained an elusive goal.

Recently, we have provided several such characterizations. The underlying idea is to bound run time in terms of an ordinary polynomial in the largest answer returned by an oracle, while imposing a constant upper bound on the number of times an oracle query (answer) may exceed all previous ones in size. The resulting classes are contained in Mehlhorn's class, and when closed under composition are in fact equivalent.

In this talk we will present these recent results and follow-up work involving new scheme-based characterizations of Mehlhorn's class, as well as a recent characterization using a tier-based type system for a simple imperative programming language with oracle calls.

(Joint work with F. Steinberg, and with E. Hainry, J.-Y. Marion, and R. Pechoux.)

Algorithmes et complexité
Mardi 7 décembre 2021, 14 heures, 3052
Daniel Szilagyi Introduction to convexity - optimization and sampling

In this talk we present some basic notions of convexity, from a quantum-algorithmic point of view. The talk will consist of two parts. We first warm-up by introducing some classical first- and second-order methods for convex optimization. Then, we move on to more structured convex problems, introduce linear programming and the basic ideas of interior-point methods. We mention some quantum algorithms for LPs and SDPs. In the second part of the talk we discuss sampling, and in particular its applications to estimating volumes of polytopes. We present the basic classical sampling algorithms (ball walk and hit-and-run), and the general framework for applying these algorithms to volume estimation. We conclude by discussing the opportunities for quantum speedups - in particular, we present a high-level overview of the work by Chakrabarti, Childs, Hung, Li, Wang and Wu from 2019.

One world numeration seminar
Mardi 7 décembre 2021, 14 heures 30, Online
Jamie Walton (University of Nottingham) Extending the theory of symbolic substitutions to compact alphabets

In this work, joint with Neil Mañibo and Dan Rust, we consider an extension of the theory of symbolic substitutions to infinite alphabets, by requiring the alphabet to carry a compact, Hausdorff topology for which the substitution is continuous. Such substitutions have been considered before, in particular by Durand, Ormes and Petite for zero-dimensional alphabets, and Queffélec in the constant length case. We find a simple condition which ensures that an associated substitution operator is quasi-compact, which we conjecture to always be satisfied for primitive substitutions on countable alphabets. In the primitive case this implies the existence of a unique natural tile length function and, for a recognisable substitution, that the associated shift space is uniquely ergodic. The main tools come from the theory of positive operators on Banach spaces. Very few prerequisites will be assumed, and the theory will be demonstrated via examples.

Théorie des types et réalisabilité
Mercredi 8 décembre 2021, 14 heures, Salle 1007
Federico Olimpieri (Université de Leeds) Categorifying Intersection Types

We study a family of distributors-induced bicategorical models of lambda-calculus, proving that they can be syntactically presented via intersection type systems. We first introduce a class of 2-monads whose algebras are monoidal categories modelling resource management. We lift these monads to distributors and define a parametric Kleisli bicategory, giving a sufficient condition for its cartesian closure. In this framework we define a proof-relevant semantics: the interpretation of a term associates to it the set of its typing derivations in appropriate systems. We prove that our model characterize solvability, adapting reducibility techniques to our setting. We conclude by describing two examples of our construction.

Combinatoire énumérative et analytique
Jeudi 9 décembre 2021, 14 heures, Salle 1007
Harriet Walsh (IRIF, Université de Paris) Non encore annoncé.

Gâteau de l'IRIF
Jeudi 9 décembre 2021, 17 heures, 3052
Clément Ducros, Sander Gribling Gâteau de l'IRIF

IRIF CakeTM is an amazing opportunity to meet people while simultaneously eating cakes baked by your fellow colleagues! Join us every Thursday, at 5pm, in front of room 3052 (Sophie Germain 3rd floor) for a weekly feast. You can also express your cooking skills and volunteer to bake a cake by sending an email to

Catégories supérieures, polygraphes et homotopie
Vendredi 10 décembre 2021, 14 heures, Salle 1007
Alain Prouté À la découverte des preuves mathématiques formelles

Dans cet exposé, je propose une méthode nouvelle pour introduire la notion de preuve mathématique formelle. Contrairement à ce qui est habituellement proposé, à savoir une introduction basée sur un postulat, comme par exemple le postulat de la correspondance de Curry-Howard, cette méthode ne suppose aucun postulat. Elle n'utilise que des faits que les mathématiciens, et en particulier les mathématiciens non logiciens, admettent sans discussion, parce que ce sont des mécanismes qu'ils utilisent tous les jours. Comme la méthode ne suppose aucune syntaxe a priori pour les preuves, la définition des preuves que je vais donner est un cadre général qui pourrait a priori accommoder différentes syntaxes de preuves. Toutefois on verra, qu'à condition de ne pas introduire de choses inutiles dans le langage, et au variations syntaxiques superficielle près, il n'y a essentiellement qu'un seul langage de preuve possible. On verra quelques exemples de preuves formelles. La méthode met aussi immédiatement en évidence l'existence d'un opérateur de choix et d'un opérateur de description. Ceci m'amènera aussi (si le temps imparti le permet) à discuter de l'axiome du choix et de son rapport au langage ainsi mis en évidence.

Vendredi 10 décembre 2021, 14 heures 30, Salle 3052
Marie Fortin (University of Liverpool) How undecidable are HyperLTL and HyperCTL*?

Temporal logics for the specification of information-flow properties are able to express relations between multiple executions of a system. Two of the most important such logics are HyperLTL and HyperCTL*, which generalise LTL and CTL* by trace quantification. It is known that this expressiveness comes at a price, i.e., satisfiability is undecidable for both logics. We settle the exact complexity of these problems, showing that both are in fact highly undecidable: we prove that HyperLTL satisfiability is \Sigma_1^1-complete and HyperCTL* satisfiability is \Sigma_1^2-complete. To prove \Sigma_1^2 membership for HyperCTL*, we prove that every satisfiable HyperCTL* formula has a model that is equinumerous to the continuum, the first upper bound of this kind. We prove this bound to be tight. This is joint work with Louwe B. Kuijer, Patrick Totzke and Martin Zimmermann.

Analyse et conception de systèmes
Vendredi 10 décembre 2021, 10 heures 30, Salle 1007
Pierre-Evariste Dagand (IRIF) Commentary on “Formal Metatheory of Second-Order Abstract Syntax”

The forthcoming edition of POPL will feature a rather elegant piece [] by M. Fiore and D. Szamozvancev on the implementation of intrinsic syntaxes in type theory, using the usual categorical tools (initial algebra semantics, presheafs, etc.) as an effective blueprint for the construction.

I propose (rather: Adrien has volunteered me) to show up with an Agda buffer and offer a live tour and commentary of the code.

Graph Transformation Theory and Applications
Vendredi 10 décembre 2021, 15 heures, online
Emilio Jesús Gallego Arias (Université de Paris, CNRS, IRIF, France) Formalizing Category Theory using Type Theory: A Discussion

Since its inception at the start of the 20th century, type theory has become a core foundational tool for those interested in the logical foundations of mathematics and computer science. A key milestone on the field is the Calculus of Inductive Constructions, the type theory that lies at the heart of modern interactive proof assistants such as Coq or Lean. The CiC is remarkably expressive, yet remains computationally tractable, leading to important milestones in computer-checked mathematical results such as the 4 color theorem or the Feit-Thompson theorem. In this talk, we will present the calculus of inductive constructions as currently implemented in the Coq proof assistant, and we will explore the encoding of basic constructions of category theory in Coq, placing a particular emphasis the usability and modularity of our definitions.

Zoom meeting registration link

YouTube live stream