Institut de Recherche en Informatique Fondamentale (IRIF)


Université Paris Cité

IRIF is a research laboratory of CNRS and Université Paris Cité, 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. Seven of its members have been distinguished by the European Research Council (ERC), six 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.

Follow us on Twitter/X, LinkedIn and Mastodon for our latest news:

LinkedIn Twitter/X Mastodon


Ahmed Bouajjani, Professor at IRIF, has been awarded for his contribution to research in the computer science field. He has been nominated in the Scientific Research category for the 6th edition of the “Trophées Marocains du Monde”. Many congratulations!

The 14th Île-de-France Programming Day will take place on Monday, June 10, 2024, at Université Paris Cité, in the Department of Computer Science. This day is an opportunity for a fun and friendly competition between teams of computer science undergraduate students from Université Paris-Saclay, Université Paris Cité, and Sorbonne University. This day is jointly organized by Pierre Letouzey (IRIF), Jean-Baptiste Yunès (UPC), Emmanuel Chailloux (UPMC) and Jean-Christophe Filliâtre (Paris Saclay).


IRIF is pleased to announce its second Distinguished Lecture of the year! Our invited speaker is Omer Reingold, professor of computer science at Stanford University and the director of the Simons Collaboration on the Theory of Algorithmic Fairness (Simons Foundation). He will talk about Algorithmic Fairness. Anyone interested is welcome to join us for this talk!

The rerun of Véronique Cortier Distinguished Talk that was held on February is now available on the IRIF YouTube channel. Her subject was: “Electronic voting: design and formal verification”.


Three scientific outreach projects by IRIF researchers have been selected for the 2024 edition of France-Paris Pint of Science. The idea is to discover a scientific theme or subject in a bar. Our researchers will be talking about data protection, graphs and quantum computing.

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

Non-permanent members' seminar
Thursday May 30, 2024, 4PM, Salle 3052 and Zoom Link
Victor Arrial The Bang-Calculus: An Accessible Introduction to Subsuming Paradigms

The lambda calculus is a formal system that serves as the foundation for functional programming languages. It supports different evaluation strategies, resembling the evaluation processes of various programming languages such as Haskell and OCaml. The Bang Calculus is an extension of the lambda calculus introduced to provide explicit counterparts for these strategies, thus allowing a uniform study of them.

In this talk, we will present the Bang Calculus and provide multiple examples of (simple) properties that can be subsumed within this framework. Absolutely no prerequisites are required.

Higher categories, polygraphs and homotopy
Friday May 31, 2024, 2PM, Salle 3058
Sacha Ikonicoff Catégories différentielles et tangentes pour les algèbres sur une opérade

La notion de catégorie différentielle cartésienne permet de formaliser dans un contexte catégorique la notion de dérivée directionnelle. Similairement, la notion de catégorie tangente fournit un analogue à la notion de fibré tangent de la géométrie différentielle dans le contexte de la théorie des catégories.
  Dans cet exposé, nous décrirons une nouvelle notion de monade différentielle cartésienne. Cette structure consiste en une monade équipée d'une transformation naturelle appelée "combinateur différentiel". Pour une telle monade, nous montrerons que la catégorie (opposée) de Kleisli associée est munie d'une structure différentielle cartésienne, et que la catégorie d'algèbres associée est munie d'une structure tangente.
  Finalement, nous considérerons l'exemple des algèbres sur une opérade. Nous montrerons que la monade associée à toute opérade (algébrique, symétrique) admet un combinateur différentiel. Nous étudierons la catégorie différentielle cartésienne et la catégorie tangente associée. Nous montrerons que cette catégorie tangente admet une structure tangente adjointe qui permet de retrouver certaines notions provenant de la géométrie algébrique et non-commutative.

Friday May 31, 2024, 2PM, Salle 3052
Thomas Colcombet Bisimulation invariant MSO over finite transition systems

In this talk, I will present a recent result obtained in collaboration with Amina Doumane and Denis Kuperberg on the properties definable in MSO which are bisimulation invariant over finite transition systems. We show that these coincide with mu-calculus-definable properties. This is a variant of a result from Janin and Walukiewicz over general (ie possibly infinite) transition systems [JW96].

Our proof techniques involve developing an algebraic theory of infinite regular trees, in particular establishing on the way that recognizable languages of regular trees coincide (over regular trees) with MSO definable language of trees.

Graph Transformation Theory and Applications
Friday May 31, 2024, 3PM, online
Kristopher Brown (Topos Institute, Berkeley, California, USA) A graphical language for programming with graph rewriting

We provide a general introduction to the AlgebraicJulia ecosystem and AlgebraicRewriting.jl, which allows for integrating general-purpose code with computation of many graph transformation constructions in a broad variety of categories. Practical applications of graph transformation depend on being able to apply sequences of rewrites in a controlled manner: we present work on a graphical language for the construction and composition of such programs, including computation of normal forms as well as scientific agent-based model simulations. This graphical language can be given semantics in many different contexts (e.g. deterministic, nondeterministic, probabilistic) and can be functorially migrated, which yields graph rewriting programs that operate in other categories.

Zoom meeting registration link

YouTube live stream

Enumerative and analytic combinatorics
Tuesday June 4, 2024, 11AM, Salle 1007
Pas De Séminaire (Mais Séminaire Flajolet Le Jeudi 6 Juin !) Pas de séminaire

Algorithms and complexity
Tuesday June 4, 2024, 11AM, Salle 3052
Kuo-Chin Chen (Foxconn Research) Quantum Walks on Simplicial Complexes and Harmonic Homology: Application to Topological Data Analysis with Superpolynomial Speedups

Incorporating higher-order interactions in information processing enables us to build more accurate models, gain deeper insights into complex systems, and address real-world challenges more effectively. However, existing methods, such as random walks on oriented simplices and homology, which capture these interactions, are not known to be efficient. This work investigates whether quantum walks on simplicial complexes exhibit quantum advantages. We introduce a novel quantum walk that encodes the combinatorial Laplacian, a key mathematical object whose spectral properties reflect the topology of the underlying simplicial complex. Furthermore, we construct a unitary encoding that projects onto the kernel of the Laplacian, representing the space of harmonic cycles in the complex's homology. Combined with the efficient construction of quantum walk unitaries for clique complexes that we present, this paves the way for utilizing quantum walks to explore higher-order interactions within topological structures. Our results achieve superpolynomial quantum speedup with quantum walks without relying on quantum oracles for large datasets.

Crucially, the walk operates on a state space encompassing both positively and negatively oriented simplices, effectively doubling its size compared to unoriented approaches. Through coherent interference of these paired simplices, we are able to successfully encode the combinatorial Laplacian, which would otherwise be impossible. This observation constitutes our major technical contribution. We also extend the framework by constructing variant quantum walks. These variants enable us to: (1) estimate the normalized persistent Betti numbers, capturing topological information throughout a deformation process, and (2) verify a specific QMA1-hard problem, showcasing potential applications in computational complexity theory.

Algorithms and complexity
Wednesday June 5, 2024, 11AM, Salle 4052 (PCQC)
Marin Costes (Université Paris-Saclay) Space-time deterministic graph rewriting

We study non-terminating graph rewriting models, whose local rules are applied non-deterministically—and yet enjoy a strong form of determinism, namely space-time determinism. Of course in the case of terminating computation it is well-known that the mess introduced by asynchronous rule applications may not matter to the end result, as confluence conspires to produce a unique normal form. In the context of non-terminating computation however, confluence is a very weak property, and (almost) synchronous rule applications is always preferred e.g. when it comes to simulating dynamical systems. Here we provide sufficient conditions so that asynchronous local rule applications conspire to produce well-determined events in the space-time unfolding of the graph, regardless of their application orders. Our first example is an asynchronous simulation of a dynamical system. Our second example features time dilation, in the spirit of general relativity.

Non-permanent members' seminar
Thursday June 6, 2024, 4PM, Salle 3052
Allen Ibiapina k-Linkage on Temporal Graphs

Given a graph \( G \) and a set of \( k \) pairs of vertices, the \( k \)-Linkage Problem asks whether there exists a set of \( k \) paths such that each path connects a given pair of vertices, and each vertex in the graph is used by at most one of these paths. When one consider temporal graphs, where the graph's structure can change over time, the \( k \)-Linkage Problem takes on new variations. This seminar focuses on a specific version where we seek time-respecting paths that connect the given pairs of vertices, ensuring that at any given time, each vertex is occupied by at most one path. I will present results on the parameterized complexity of this problem when \( k \) is given as a parameter.

Syntax Meets Semantics
Thursday June 6, 2024, 2PM, Salle 3071
Adrienne Lancelot (LIX Polytechnique and IRIF UPC) Mirroring Call-by-Need, or Values Acting Silly

Call-by-need evaluation for the lambda-calculus can be seen as merging the best of call-by-name and call-by-value, namely the wise erasing behaviour of the former and the wise duplicating behaviour of the latter. To better understand how duplication and erasure can be combined, we design a degenerated calculus, dubbed call-by-silly, that is symmetric to call-by-need in that it merges the worst of call-by-name and call-by-value, namely silly duplications by-name and silly erasures by-value.

We validate the design of the call-by-silly calculus via rewriting properties and multi types. In particular, we mirror the main theorem about call-by-need – that is, its operational equivalence with call-by-name – showing that call-by-silly and call-by-value induce the same contextual equivalence. This fact shows the blindness with respect to efficiency of call-by-value contextual equivalence. We also define a call-by-silly strategy and measure its length via tight multi types. Lastly, we prove that the call-by-silly strategy computes evaluation sequences of maximal length in the calculus.

Friday June 7, 2024, 2PM, Salle 3052
Lê Thành Dũng (Tito) Nguyễn Computing the polynomial degree of size-to-height increase for macro tree transducers

In a paper to appear at ICALP'24 [*], Gallot, Maneth, Nakano and Peyrat show that, given a tree-to-tree function f computed by a macro tree transducer (a natural register-based machine model, which will be recalled in the talk), the following problems are decidable: (1) is height(f(t)) = O(height(t)) ? (2) is height(f(t)) = O(size(t)) ? We sketch a tentative proof of a generalization of (2) by different and arguably simpler means. More precisely, we show that the quantity inf {k | height(f(t)) = O(size(t)^k)} ∈ ℕ∪{+∞} is computable by reduction to ambiguity of (ordinary) tree automata. (Joint work with Paul Gallot and Nathan Lhote, in preparation.) [*]