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. Six 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.

Article Blog Binaire- Contrôle accès Site Porno

Geoffroy Couteau et Pierre-Evariste Dagand ont écrit un texte à quatre mains dans le Blog Binaire du Journal Le Monde. Ils se demandent s'il est possible de contrôler l'accès aux sites pornographiques tout en conservant l'anonymat et les données de l'utilisateur pour protéger les enfants. C'est ici que le “zéro-proof knowledge” rentre en jeux…

Journées PPS 2023

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


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 :

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


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.

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.

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 ?

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

Monday June 5, 2023, 11AM, 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.

Monday June 5, 2023, 2PM, 146 (Olympe de Gouges)
Wendlasida Ouedraogo (INRIA (Paris Saclay)) Source code optimization for safety critical systems

A computer system is safety-critical when it can cause serious damage to property, the environment, human life, or to society as a whole. Real-world safety-critical systems are also necessarily complex, because, to take into account the interactions between software, hardware, the physical environment, and sometimes their distributed nature (systems of systems), they need to implement a variety of safety measures, in software, hardware, in the system design, at development time, at compile time, and at run-time. Those safety measures which vary from one safety-critical system to another very often lead to a decrease in performance, for a increase in the execution time of software.

This research work is situated in the context of one such system, the communication-based train control (CBTC) system of Siemens Mobility France which operates a number of driverless subway systems around the World, including Paris lines 1, 4, and 14. That system is certified according to the industrial norm EN-50128 and up to the highest Safety Integrity Level 4, required for safety-critical systems with potentially catastrophic consequences. In this context, the thesis looks for an answer to the question of how to automatically optimize the execution time performance of such systems without losing the previously obtained safety guarantees.

The answer provided is provably correct optimization of source code. A first contribution is a source-to-source compiler for VCP Ada (a subset of Ada) programs, that optimizes source code while preserving the formal semantics of the programs. The compiler has been proven correct in the Coq proof assistant and guarantees the equivalence of execution between the original and the optimized program. The compiler copes with the complexities of the platform, due to hardware safety measures, which is important, since real-world safety-critical systems are often susceptible to having such measures, potentially conflicting with existing formally proven optimizing compilers. Moreover, choosing the approach of a source-to-source compilation shows to have methodological advantages over an approach to proven optimizations having a number of intermediate languages, allowing to simplify and diminishing the needed proof effort.

A second contribution is to the problem of provably correct lexical analysis of compilers, which has previously not received a lot of research attention, a weak link in any compilation chain using a proven or qualified compiler. We develop CoqLex, the first Coq-formalized lexer generator, based on a modification of an existing Coq implementation of regular expression matching via Brzozowski derivatives.

The developed theory and tools have been applied to optimize real-world VCP Ada programs of CBTC systems, consisting of thousands of source files, with promising results.

Algorithms and complexity
Tuesday June 6, 2023, 11AM, Salle 147 (Olympe de Gouges)
Galina Pass (QuSoft, University of Amsterdam) (No) Quantum space-time tradeoff for USTCON

The problem of undirected st-connectivity is important both for its applications in network problems, and for its theoretical connections with logspace complexity. Classically, a long line of work led to a time-space tradeoff of T=Õ(n^2/S) for any S such that S=Ω(log(n)) and S=O(n^2/m), where T is the running time and S is the used space. In this talk, I will present a surprising result that quantumly there is no nontrivial time-space tradeoff: there is a quantum algorithm that achieves both optimal time Õ(n) and optimal space O(log(n)) simultaneously. This improves on previous results, which required either O(log(n)) space and Õ(n^1.5) time, or Õ(n) space and time. To complement this, we show that there is a nontrivial time-space tradeoff when given a lower bound on the spectral gap of a corresponding random walk.

Analysis and conception of systems
Wednesday June 7, 2023, 2PM, 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

Enumerative and analytic combinatorics
Thursday June 8, 2023, 2PM, Olympe de Gouges
Davig Forge (Orsay) TBD

Non-permanent members' seminar
Thursday June 8, 2023, 4PM, Olympe de Gouges 147 and Zoom link
Bernardo Jacobo-Inclan To be announced.

Friday June 9, 2023, 2PM, Salle 146 Olympe de Gouges
Daniel Smertnig Deciding Sequential? and Unambiguous? for weighted automata over fields

Previous work reduces the problem of deciding whether a weighted finite automaton (WFA) over a field is equivalent to a sequential, respectively, unambiguous, WFA to the computation of the linear hull. The linear hull is the topological closure of the reachability set in a certain linear version of the Zariski topology. We discuss an algorithm to compute the linear hull that works essentially entirely in the realm of linear algebra (i.e., without first resorting to the computation of the finer Zariski topology). Further, we show how this leads to double-exponential bounds on the size of the linear hull.

This talk is on joint work with J. Bell.

Monday June 12, 2023, 11AM, Olympe de Gouges 146 and Zoom link
Themistoklis Melissourgos (University of Essex) To be announced.

Distributed algorithms and graphs
Tuesday June 13, 2023, 3PM, 147 Olympe de Gouges
Anna Gujgiczer (Budapest University of Technology and Economics, Hungary) Circular chromatic number of generalised Mycielski graphs on odd cycles and other quadrangulations of the projective plane

Generalised Mycielskians of odd cycles are relatively small graphs with high odd girth and chromatic number 4. In the literature there are many proofs using different techniques, like methods from algebraic topology, to show the second property. It is also proven by DeVos et al that these graphs have circular chromatic number 4. Using a result from about the same time of Simonyi and Tardos, namely that for a “topologically t-chromatic” graph $G$, where $t$ is even we have $\chi_c(G) = \chi(G) = t$, one can also get this strengthened statement.

In this talk we present a new, relatively short direct proof for the circular chromatic number, using only a basic notion of algebraic topology, namely the winding number. Then we present another graph family with high odd girth and circular chromatic number 4. This construction is very similar to the generalized Mycielski, but on its first two layers it forms a M$\ddot{o}$bius ladder. We prove the statement about their circular chromatic number with similar techniques. Moreover we present a similar result for a family of signed graphs.

This talk is based on a joint work with Reza Naserasr (Universit´e de Paris, IRIF, CNRS, F-75006, Paris, France), S Rohini (Indian Institute of Technology Madras, India) and S Taruni (Indian Institute of Technology Dharwad, India).

Enumerative and analytic combinatorics
Thursday June 15, 2023, 2PM, Salle 146 - Olympe de Gouges
Marc Noy (UPC (Espagne)) Chordal graphs with bounded tree-width